Dana Scott's Favorite Completeness Proof

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.

1. 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.

2. If a formula is not provable, then it is not a tautology.

We need three lemmata about provable formulae. The symbols $latex T$ and $latex F$ are for true and false. We write negation here as $latex \lnot p$.

1. $\vdash p \rightarrow [\phi(p) \leftrightarrow \phi(T)]$.
2. $\vdash \lnot p \rightarrow [\phi(p) \leftrightarrow \phi(F) ]$.
3. If $latex \phi$ has no propositional variables, then either $latex \vdash \phi \leftrightarrow T$ or $latex \vdash \phi \leftrightarrow F$.

All these are proved by induction on the structure of $latex \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 $latex \vdash \phi(T)$ and $latex \vdash \phi(F)$, then $latex \vdash \phi(p)$. Hence if $latex \phi(p)$ is not provable, then one of $latex \phi(T)$, $latex \phi(F)$ is not provable.

So, if a formula $latex \phi$ has no propositional variables and is not provable, then by (iii), $latex \phi \leftrightarrow F$. So it is not a tautology. Arguing now by induction on the number of propositional variables in the formula, if $latex \phi(p)$ is not provable, then one of $latex \phi(T)$, $latex \phi(F)$ is not a tautology. And so $latex \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 $latex n$ variables can be proved in $latex 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.