Completeness proof (easy) More about first order logic

This page gives an alternative proof that propositional natural deduction (that is, the natural deduction calculus without the rules for quantifiers) is complete for the propositional logic defined by the two-valued truth tables for the connectives. It is simpler that the standard proof, and may be easier to grasp on a first reading, but it is less powerful in the sense that the proof technique does nor generalise to other important logics whereas the standard technique does.

We begin by defining the notion of a literal basis for a formula A. This is a set of literals (that is, atoms such as p and negated atoms such as NOTq) containing, either negated or unnegated, every atom in A. For instance, the set {NOTp, q, r} is a literal basis for the formula (p AND q) IMP (p AND r) . The set {p, q, NOTr} is another literal basis for the same formula. We stipulate that each literal basis must be consistent: that is, no atom occurs both negated and unnegated in it.

One more piece of useful notation: where β is any literal basis, let I_β be the corresponding assignment of truth values to the atoms occurring (negated or unnegated) in β. That is, I_β(p) = 1 if p ∈ β, and I_β(p) = 0 if NOTp ∈ β (and similarly for every other atom).

Now, observe two facts:

1. If β is a literal basis for A then either β ⊢ A or β ⊢ NOTA.
2. Where β is a literal basis for A, if β ⊢ A, then A is true for I_β, while if β ⊢ NOTA, than A is false for I_β.

Fact 1 is proved by observing first that it is trivially true if A is an atom, and then that it extends up from the atoms to larger and larger subformulae of A and ultimately to A itself.¹ For example, consider a subformula B IMP C with 'IMP' as its main connective. If we know that either β ⊢ B or β ⊢ NOTB, and also that either β ⊢ C or β ⊢ NOTC, then we may observe that either   β ⊢ B IMP C   or   β ⊢ NOT(B IMP C)   in virtue of the sequents:

NOTB   ⊢   B IMP C
C   ⊢   B IMP C
B, NOTC   ⊢   NOT(B IMP C)

The cases of the other connectives are similar.

Fact 2 is even easier to show. Clearly all the literals in β are true for I_β, so Fact 2 follows from Fact 1 and the soundness of the deductive system.

Now we want to show that every valid sequent is provable. In fact, we turn this around and show that every unprovable sequent is invalid. Suppose, then, that X is some set (possibly infinite) of formulae, and A is a formula such that that there is no derivation of A from X. We need to define an assignment of truth values to atoms for which everything in X is true but A is false.

Let the atoms of our propositional language be p₁, p₂, p₃, ..., etc. We build up the required interpretation incrementally by defining a sequence Y₀, Y₁, Y₂, ... of sets of literals, each one extending the previous one by adding the next atom or its negation:

Y₀ = ∅

If   X, Y_i, p_i+1 ⊢ A   then  Y_i+1 = Y_i ∪ {NOTp_i+1}.  Otherwise  Y_i+1 = Y_i ∪ {p_i+1}

Now let Y be the union of all of these sets Y₀, Y₁, Y₂, .... Clearly, by construction, any literal p_i or NOTp_i is in Y iff it is in Y_i, and iff it is in Y_j for every j ≥ i.

It is not hard to see that there is no n such that X,Y_n ⊢ A, since if there were, there would have to be a first such n. Obviously, this can't be 0, since X ∪ Y₀ is X. But it can't be any i+1 either, because this would require both X, Y_i, p_i+1 ⊢ A   and X, Y_i, NOTp_i+1 ⊢ A   and hence X, Y_i ⊢ A  , contradicting the assumption that Y_i+1 is the first set to yield A.

Let B be any formula in X. Although X may be infinite, and may contain every atom in the language, B is a particular (finite) formula, so its atoms are all among the first n for some finite n. That means that Y_n is a literal basis for B, so by Fact 1 above, either Y_n ⊢ B or Y_n ⊢ NOTB. But we can't have Y_n ⊢ NOTB because that would make X ∪ Y_n inconsistent, which it isn't because it does not imply A. Therefore Y_n ⊢ B and therefore Y ⊢ B. In a similar way, there are numbers m be such that the variables in A are all among  {p₁,...,p_m}. Since, as observed, A is not derivable from Y_m, it must be the case that Y_m ⊢ NOTA and so Y ⊢ NOTA.

By Fact 2, then, every formula in X is true for I_Y, while A is false for I_Y. We therefore have a truth value assaignment invalidating the sequent, finishing the proof of completeness.

1   That is, in the jargon, Fact 1 is proved by induction on the structure of A.