Completeness proof More about first order logic
This is a technical aside to the Logic Notes, containing a proof of a fact asserted in the body of the notes. It may be skipped by anyone willing to take that assertion on trust, as it assumes rather more mathematical background than is required to follow the general exposition of logic.
The result is the completeness of the natural deduction calculus for propositional logic as defined by truth table semantics. That is, we show that every propositional sequent which is valid according to truth tables is provable using the natural deduction rules for connectives. The basic technique will be to consider an arbitrary unprovable sequent with premises X and conclusion C, and find an assignment of truth values to the atoms which makes everything in X true but C false.
In fact, this result is so central to logic that we prove it twice! Below is the standard proof, much as it occurs in almost every introduction to mathematical logic. As an aside, however, here is an easier proof which delivers the same theorem more simply, but has the drawback that it is parochial to classical truthtable logic and does not generalise to full first order logic or to nonclassical systems as considered in Chaper 7.
We begin by considering a complete list of the formuae of propositional logic. It does not matter in what order they appear, as long as every formula occurs in the list exactly once. There is no need to give a recipe for actually constructing such a list: it is enough to note that it could be done in principle, and to let
A_{1}, A_{2}, A_{3}, ...
be an enumeration of the formulae, so every propositional formula is A_{n} for some n. In terms of this, we define a corresponding list of sets of formulae
σ_{0}, σ_{1}, σ_{2}, σ_{3}, ...
as follows:
σ_{0} = ∅
If X, σ_{i}, A_{i+1} ⊢ C then σ_{i+1} = σ_{i}. Otherwise σ_{i+1} = σ_{i} ∪ {A_{i+1}}
Now let Σ be the union of all of these sets σ_{i}. That is, Σ is the set of formulae A such that A ∈ σ_{i} for some i. Clearly, by construction, any formula A_{i} is in Σ iff it is in σ_{i}, and iff it is in σ_{j} for every j ≥ i.
Now Σ has some very nice properties. Observe the following:

For any i, there is no derivation of C
from σ_{i} ∪ X.

C is not derivable from Σ.

X is a subset of Σ.

For any A, if A ∉ Σ then
Σ, A ⊢ C.
 For any A, if Σ ⊢ A then A ∈ Σ.
Proofs of these facts are not very difficult.

Note first that C is not derivable from
σ_{0}
∪ X, because
σ_{0} ∪ X
= X. Then the nonderivability
of C extends from
σ_{i} to
σ_{i+1} because if C
would be derivable given the addition
of A_{i+1}
then A_{i+1} does not get
added, and σ_{i+1} is the same
as σ_{i}. So the
nonderivability of C is preserved throughout
the construction.

If there were a derivation of C from Σ,
this would also have to be a derivation from one of the
sets σ_{i}, because any
derivation is finite and so can only use finitely many
members of Σ, which are all in
σ_{i} where i is any
upper bound on the subscripts of the formulae
used. But C is underivable from
σ_{i}, as just
observed.

Suppose A is a formula in X. It must
be A_{i+1} for
some i ≥ 0, in which
case the set X ∪
σ_{i} ∪
{A_{i+1}} is nothing
but X ∪
σ_{i}. By observation 1,
this does not have C as a consequence,
so A_{i+1} ∈
σ_{i+1} and
hence A_{i+1}
∈ Σ.

Let A be A_{i+1}, and
suppose A ∉
Σ.
Then A_{i+1}
∉ σ_{i+1}, which can
only happen if there is a derivation of C
from X ∪
σ_{i} ∪
{A_{i+1}}. But
both X and σ_{i} are
subsets of Σ,
and A_{i+1} is A,
so Σ, A
⊢ C as required.
 If Σ ⊢ A and A ∉ Σ then by fact 4 we have Σ ⊢ A and Σ, A ⊢ C, in which case by cut we have Σ ⊢ C, contradicting fact 2. Hence if Σ ⊢ A then A ∈ Σ.
In the light of facts 4 and 5, Σ is extremely wellbehaved with respect to the connectives. Specifically, for any formulae A and B:

NOTA ∈ Σ
iff A ∉
Σ

A AND B ∈
Σ iff
A ∈ Σ
and B ∈ Σ

A OR B ∈
Σ iff
A ∈ Σ
or B ∈ Σ
 A IMP B ∈ Σ iff A ∉ Σ or B ∈ Σ
For the first of these, concerning negation, note that since Σ does not imply C, it must be consistent, so clearly if NOTA ∈ Σ then A ∉ Σ. Conversely, if neither A nor NOTA is in Σ then by fact 4, Σ, A ⊢ C and Σ, NOTA ⊢ C. But then by two applications of the rule RAA, Σ, NOTC ⊢ NOTA and Σ, NOTC ⊢ NOTNOTA so by RAA again, Σ ⊢ NOTNOTC and hence Σ ⊢ C. It follows that if A ∉ Σ, then NOTA ∈ Σ.
The second, stating that conjunction behaves as expected, is a trivial consequnce of fact 5 and the rules ANDI and ANDE.
For the third, concerning disjunction, the righttoleft direction is trivial from fact 5 and ORI. The converse follows from closure under ORE: suppose neither A nor B is in Σ; then Σ, A ⊢ C and Σ, B ⊢ C, so by ORE, Σ, A OR B ⊢ C, so A OR B ∉ Σ.
Lastly, we consider the logic of 'IMP'. If either NOTA or B is in Σ then in virtue of fact 5 and the provable sequents
B ⊢ A IMP B
NOTA ⊢ A IMP B
it follows that A IMP B is in Σ. Conversely, suppose A IMP B ∈ Σ. Either A ∈ Σ or A ∉ Σ, but if A ∈ Σ then Σ contains both A and A IMP B, and so contains B as a result of IMPE, so A ∉ Σ or B ∈ Σ as required.
Now we are in the process of defining an assignment of truth values to atoms so as to make all formulae in X true but C false. Not too surprisingly, we choose to assign 1 (true) to those atoms in Σ and 0 (false) to those not in Σ. By appeal to the observations just made, it is easy to see that for every formula A, A is true for this interpretation iff A ∈ Σ. Since X is a subset of Σ, and clearly C is not in Σ, this finishes the proof of completeness.
The general technique for this type of completeness proof is to show that every valid sequent is provable by showing the contrapositive: that every unprovable sequent is invalid. This is done by considering an arbitrary unprovable sequent and "cooking up" an invalidating interpretation out of the formulae involved. The extension of the consistent set X to the maximal consistent set Σ is a construction commonly found in completeness proofs. The fact that every consistent set has a maximal consistent superset is known as Lindenbaum's lemma, and it holds for a wide range of logical systems.