Kalmár’s Compleness Proof

Dana Scott’s proof reminded commenter “fbou” of Kalmár’s 1935 completeness proof. (Original paper in German on the Hungarian Kalmár site.) Mendelsohn’s Introduction to Mathematical Logic also uses this to prove completeness of propositional logic. Here it is (slightly corrected):

We need the following lemma:

Let \(v\) be a truth-value assignment to the propositional variables in \(\phi\), and let \(p^v\) be \(p\) if \(v(p) = T\) and \(\lnot p\) if \(v(p) = F\). If \(v\) makes \(\phi\) true, then \[p_1^v, \dots, p_n^v \vdash \phi.\]

This is proved by induction on complexity of \(\phi\).

If \(\phi\) is a tautology, then any \(v\) satisfies \(\phi\). If \(v\) is a truth value assignment to \(p_1, \dots, p_n\), let \(\Gamma(v,k) = {p_1^v, \dots, p_k^v}\). Let’s show that for all \(v\) and \(k = n, \dots, 0\), \(\Gamma(v, k) \vdash \phi\). If \(k = n\), then \(\Gamma(v, n) \vdash \phi\) by the lemma and the assumption that \(\phi\) is a tautology, i.e., true for all \(v\). Suppose the claim holds for \(k+1\). This means in particular \(\Gamma(v, k) \cup {p_{k+1}} \vdash \phi\) and \(\Gamma(v, k) \cup {\lnot p_{k+1}} \vdash \phi\) for any given \(v\). By the deduction theorem, we get \(\Gamma(v, k) \vdash p_{k+1} \to \phi\) and \(\Gamma(v, k) \vdash \lnot p_{k+1} \to \phi\). By \(\vdash p_{k+1} \lor \lnot p_{k+1}\) and proof by cases, we get \(\Gamma(v, k) \vdash \phi\).  The theorem then follows since \(\Gamma(v, 0) = \emptyset\).


  • The inductive proof of the lemma requires as inductive hypothesis both the claim and the corresponding claim for the case where \(v\) makes \(\phi\) false (i.e., that then \(p_1^v, \dots, p_n^v \vdash \lnot \phi\)). Kalmár did not include the constants \(T\) and \(F\) in the language, but if you would, then Scott’s (iii) would be a special case of the lemma.
  • Scott’s proof does not require the deduction theorem, but does require proof of substitutability of equivalents.

Leave a Reply

Your email address will not be published. Required fields are marked *