At Wikipedia/Propositional_Calculus I found the following proof sketch of the completeness of propositional logic systems which (among other things, I assume) admit the proof-by-case-analysis formula $(p \to s) \to ((\lnot p \to s) \to s)$:
If a formula is a tautology, then there is a truth table for it which shows that each valuation yields the value true for the formula. Consider such a valuation. By mathematical induction on the length of the subformulas, show that the truth or falsity of the subformula follows from the truth or falsity (as appropriate for the valuation) of each propositional variable in the subformula. Then combine the lines of the truth table together two at a time by using "(P is true implies S) implies ((P is false implies S) implies S)". Keep repeating this until all dependencies on propositional variables have been eliminated. The result is that we have proved the given tautology. Since every tautology is provable, the logic is complete.
I don't quite follow this. Let me try an example: we wish to apply this method to prove the hypothesis introduction formula $a \to (b \to a)$ [which will likely lead to circular reasoning if it's an axiom in our system, but let's ignore that].
First we split it up into subformulae $a$ and $b \to a$ and prove their truth valuations from the truth assignments of their variables; so $a \to a$ and $\lnot a \to \lnot a$ (this assumes that we can prove reflexivity of implication, $p \to p$). We also recur on $b \to a$ and show $b \to b$ and $\lnot b \to \lnot b$, and repeat the proof for a.
Then, having conditionally proven the leaf formulae, we construct a proof that $(b \to a)$ has the truth value it has when its subformulae (variables) have the values they have, e.g. we prove the four following statements:
- $\lnot a \to \lnot b \to (b \to a)$
- $\lnot a \to b \to \lnot (b \to a)$
- $a \to \lnot b \to (b \to a)$
- $a \to b \to (b \to a)$
Questions: Is it really these four? How do we prove them?
Having proven them, I see how the case analysis theorem lets us combine statements 1 and 3 into $(\lnot b \to (b \to a))$, but it doesn't apply to 2 and 4 because they have opposite conclusions.
Question: What's the induction step being hinted at in the quote? Does it work at all?
It seems to me like this is a clumsy restatement of the completeness proof by Kalmar from 1935. Am I off base?