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:

  1. $\lnot a \to \lnot b \to (b \to a)$
  2. $\lnot a \to b \to \lnot (b \to a)$
  3. $a \to \lnot b \to (b \to a)$
  4. $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?

  • 1
    $\begingroup$ The extract from the Wikipedia article is extremely badly written and unclear. The idea is that for any given assignment of truth values to the propositional variables of a formula (say $a$ is true and $b$ is false in your example of the formula $a \to (b \to a)$), you can find a proof that that assignment results in the same truth value for the formula as is given by the truth table (i.e., a proof that $a \to \lnot b \to (a \to (b \to a)$ in this case in your example). Now repeated use of proof by case analysis shows that a formula that is validated by the method of truth tables is provable. $\endgroup$
    – Rob Arthan
    Jul 30, 2017 at 21:19
  • $\begingroup$ The complete proof is in Elliott Mendelson, Introduction to Mathematical Logic, CRC Press (6th ed 2015), page 34-35. $\endgroup$ Jul 31, 2017 at 13:39
  • 1
    $\begingroup$ And you are right: it is Kalmar's 1935 proof. $\endgroup$ Jul 31, 2017 at 13:56

1 Answer 1


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


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .