Completeness IV Metalogic

This is another proof of 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.

The proof given below is the standard one, similar to those found in almost all introductions to mathematical logic. The reason for includig it in these notes, despite the fact that we have already (several times) established the result, is that it generalises readily to full first order logic with quantifiers, and can be adapted to deal with a wide range of non-classical logics as well.

We begin by considering a complete list of the formulae 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 such a total ordering of the formulae exists in principle, so 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}

That is, we build up a collection of formulae, putting each one in the collection as long as by so doing we avoid the unwanted conclusion C.

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:

Proofs of these facts are not very difficult: click on them to see.

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 ∉ Σ

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 ∈ Σ.

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

The fact that conjunction behaves as expected is almost trivial. Since Σ is closed under ANDE, if it contains A AND B then it contains both conjuncts A and B. Conversely, if it contains both A and B, then by ANDI it contains their conjunction A AND B.

A OR B ∈ Σ   iff   A ∈ Σ or B ∈ Σ

The case of disjunction is almost as obvious as that of conjunction.. 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 ∉ Σ.

A IMP B ∈ Σ   iff   A ∉ Σ or B ∈ Σ

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 most completeness proofs, exemplified by this and the two previous ones, 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.