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

A1, A2, A3, ...

be an enumeration of the formulae, so every propositional formula is An 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, Ai+1 ⊢ C   then σi+1 = σi.  Otherwise σi+1 = σi ∪ {Ai+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 Ai is in Σ iff it is in σi, and iff it is in σj for every ji.

Now Σ has some very nice properties. Observe the following:

  1. For any i, there is no derivation of C from σiX.
  2. C is not derivable from Σ.
  3. X is a subset of Σ.
  4. For any A, if A ∉ Σ then  Σ, AC.
  5. For any A, if  Σ ⊢ A  then A ∈ Σ.

Proofs of these facts are not very difficult.

  1. Note first that C is not derivable from σ0X, because σ0X = X. Then the non-derivability of C extends from σi to σi+1 because if C would be derivable given the addition of Ai+1 then Ai+1 does not get added, and σi+1 is the same as σi. So the non-derivability of C is preserved throughout the construction.
  2. 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.
  3. Suppose A is a formula in X. It must be Ai+1 for some i ≥ 0, in which case the set X ∪ σi ∪ {Ai+1} is nothing but X ∪ σi. By observation 1, this does not have C as a consequence, so Ai+1 ∈ σi+1 and hence Ai+1 ∈ Σ.
  4. Let A be Ai+1, and suppose A ∉ Σ. Then Ai+1 ∉ σi+1, which can only happen if there is a derivation of C from X ∪ σi ∪ {Ai+1}. But both X and σi are subsets of Σ, and Ai+1 is A, so Σ, AC as required.
  5. If Σ ⊢ A  and A ∉ Σ then by fact 4 we have  Σ ⊢ A  and  Σ, AC, 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,  Σ, AC  and  Σ, NOTAC. 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  Σ, AC  and  Σ, BC,  so by ORE,  Σ, A OR BC,  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


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.