Last week I gave my decision problem talk at Berkeley. I briefly mentioned the 1917/18 Hilbert/Bernays completeness proof for propositional logic. It (as well as Post’s 1921 completeness proof) made essential use of provable equivalence of a formula with its conjunctive normal form. Dana Scott asked who first gave (something like) the following simple completeness proof for propositional logic:
We want to show that a propositional formula is provable from a standard axiomatic set-up iff it is a tautology. A simple corollary will show that if it is not provable, then adding it as an axiom will make all formulae provable.
- If a formula is provable, then it is a tautology.
Because the axioms are tautologies and the rules of inference (substitution and detachment) preserve being a tautology. The argument is by induction on the length of the proof.
- If a formula is not provable, then it is not a tautology.
We need three lemmata about provable formulae. The symbols \(T\) and \(F\) are for true and false. We write negation here as \(\lnot p\).
- $\vdash p \rightarrow [\phi(p) \leftrightarrow \phi(T)]$.
- $\vdash \lnot p \rightarrow [\phi(p) \leftrightarrow \phi(F) ]$.
- If \(\phi\) has no propositional variables, then either \(\vdash \phi \leftrightarrow T\) or \(\vdash \phi \leftrightarrow F\).
All these are proved by induction on the structure of \(\phi\) and require checking principles of substitutivity of equivalences. And I am claiming here this is less work than formulating and proving how to transform formulae into conjunctive normal form.
From (i) and (ii) it follows that: \[\vdash \phi(p) \leftrightarrow [ [ p \rightarrow \phi(T) ] \land [\lnot p \rightarrow \phi(F)] ],\] because we can show generally: \[\vdash \psi \leftrightarrow [ [ p \rightarrow \psi ] \land [ \lnot p \rightarrow \psi ] ].\] Thus, we can conclude: if \(\vdash \phi(T)\) and \(\vdash \phi(F)\), then \(\vdash \phi(p)\). Hence if \(\phi(p)\) is not provable, then one of \(\phi(T)\), \(\phi(F)\) is not provable.
So, if a formula \(\phi\) has no propositional variables and is not provable, then by (iii), \(\phi \leftrightarrow F\). So it is not a tautology. Arguing now by induction on the number of propositional variables in the formula, if \(\phi(p)\) is not provable, then one of \(\phi(T)\), \(\phi(F)\) is not a tautology. And so \(\phi(p)\) is not a tautology. QED
I don’t know the answer. Do you?
The only thing it reminded me of was this old paper which shows that all tautologies in \(n\) variables can be proved in \(f(n)\) steps using the schema of equivalence. It uses a similar idea: evaluate formulas without variables to truth values, and then inductively generate the tautologies by induction on the number of variables and excluded middle. You could turn that proof into a completeness proof by establishing for a given calculus that the required equivalences and formulas are provable.
Dana’s proof is a lot simpler, though. Thanks to him for allowing me to post his question here.