Induction in the proof of soundness theorem

Question

The statement of the soundness theorem in both propositional and predicate logic is as follows:

$\Sigma \vdash \alpha \rightarrow \Sigma \vDash \alpha$ for $\Sigma \subseteq W, \alpha \in W$ where $W$ is the set of well formed formulas of our language, and suppose that our axiom system is $T$, the set of all tautologies. I want to prove the theorem, and it seems the most common tactic (and has been suggested to me) is to use induction on the length of $\alpha.$ Since $\Sigma \vdash \alpha$, there must have been some deduction sequence $(\alpha_1,\alpha_2,\alpha_3,....\alpha_n=\alpha)$ for $\alpha_i \in \Sigma$. Then, each $\alpha_i$ has arisen from one of the following:

1. $\alpha_i$ was part of the hypotheses,
2. $\alpha_i$ is a tautology
3. $\alpha_i$ followed from an earlier $\alpha_j$ by the way of modus ponens.

If $\alpha$ falls into one of the first 2 categories we are finished. Then through the process of elimination we want to use induction should $\alpha$ occur as the result of modus ponens. How exactly is this accomplished? It seems that there are many ways for $\alpha_i$ to follow as a result of modus ponens - perhaps it is the result of $\alpha_j \rightarrow \alpha_i$, or perhaps $\alpha_j \iff \alpha_i$ or maybe even $(\alpha_k \rightarrow \alpha_j) \rightarrow \alpha_i$. How many cases are there?

Answer 1

As Mauro suggests, the induction works on the length of the derivation of $\alpha$. In other words, the induction happens on the number of steps of the proof of the (well-formed) formula.

So, let's say the length of the derivation is 0. This makes for the base case, where we have an axiom which is already a known tautology.

Now, suppose that soundness holds for any derivation with n steps. We'll show that a derivation with one more step will also be a tautology. A derivation with one more step, for it's S(n) step (the successor step to n) will either

1. Instantiate an axiom. In such a case, the next step is a tautology. Since all previous steps were tautologies, all members of the proof are tautologies and the result follows.
2. Instantiate a previously proven theorem in the sequence. In such a case, the next step being an instance of a tautology is also a tautology. So, again, since all previous steps were tautologies, all members of the proof are tautologies and the result follows.
3. Follow by the use of modus ponens from previous steps in the sequence. Now, the previous steps would be some conditional and the antecedent of that conditional. But, by the induction hypothesis, since they are previous steps, both are tautologies. And when A and (A$\rightarrow$B) are tautologies, so is B. B is the new step in this case. Since all previous steps were tautologies, and the new step is also a tautology, it follows that all members of the proof are tautologies.

That covers all possible cases. Therefore, by induction on the length of the derivation of the formula $\alpha$, the soundness meta-theorem follows.