completeness of propositional logic from $(a \to b) \to ((\lnot a \to b) \to b)$ 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?
 A: Having read (most of) Kalmar's proof, I know what's missing from the quoted fragment.
There's a sketch of half of the real proof at https://people.ucalgary.ca/~rzach/blog/2014/11/kalmars-compleness-proof.html.
Part one: if $a, \ldots, z \vdash \varphi$ and $a, \ldots, \lnot z \vdash \varphi$ then $a, \ldots, y \vdash \varphi$ (where $a, \ldots, y$ can be negated or not). This is shown using the deduction theorem to conclude $a, \ldots, y \vdash z \to \varphi$ and $a, \ldots, y \vdash (\lnot z) \to \varphi$. Using the case analysis formula, one concludes $z$. By induction one eliminates all assumptions.
This assumes we can construct a proof of $z \to \varphi$ and $(\lnot z) \to \varphi$ under assumptions $a, \ldots, y$ where this implication holds. In Kalmar's proof, he uses various axioms to construct such proofs, working inductively in the height of $\varphi$.


*

*Kalmar uses $\alpha \to \lnot \lnot \alpha$ when $\varphi$ is a negation

*Kalmar uses $(\lnot \alpha) \to (\alpha \to \beta)$ and $\alpha \to \beta \to \alpha$ and $\alpha \to (\lnot \beta) \to \lnot (\alpha \to \beta)$ when $\varphi$ is an implication.

*Kalmar uses $(\alpha \to (\beta \to \gamma)) \to (\alpha \to \beta) \to (\alpha \to \gamma)$ to show $\alpha \to \alpha$, which is used in one of the cases.


Thus, it does not immediately follow that case analysis plus deduction theorem (e.g. via S and K combinator axioms) is a complete system.
Kalmar's article is available at http://www.inf.u-szeged.hu/projectdirs/kalmar/pdf/35_act_sci_math.pdf
