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:
- $\alpha_i$ was part of the hypotheses,
- $\alpha_i$ is a tautology
- $\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?