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 truth-table logic and does not generalise to full first order logic or to non-classical 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₁, A₂, A₃, ...

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

σ₀, σ₁, σ₂, σ₃, ...

as follows:

σ₀ = ∅

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 σ₀ ∪ X, because σ₀ ∪ X = X. Then the non-derivability 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 non-derivability 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 well-behaved 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 right-to-left 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.