Completeness I Metalogic

Our goal in this section is to prove that every sequent which is valid according to the defined semantics for classical logic also has a proof in the natural deduction calculus. For the present, we confine attention to propositional logic, leaving the technical care and feeding of quantifiers for later.

The first part of this proof is little more than an observation. Given any finite sequent with premises A₁, ..., A_n and conclusion B, we can appeal to the deduction equivalence n times to find an equivalent single formula

A₁ IMP (... IMP (A_n IMP B))

which is a theorem if and only if the original sequent is provable, and is a tautology iff the original sequent is valid. Now we already know from Chapter 2 that every propositional formula has an equivalent (i.e. with the same truth table) in conjunctive normal form (CNF). Let us call that CNF formula C. We also know that equivalent formulae can replace each other in any context, and we have the Diligent Reader's assurance that the equivalences required for every step of the reduction to CNF can all be proved by natural deduction. Hence we know there is a provable sequent

C   TS   A₁ IMP (... IMP (A_n IMP B))

If C is a theorem, then

TS   A₁ IMP (... IMP (A_n IMP B))

and hence by n applications of IMPE:

A₁, ..., A_n   TS   B

Hence, to show that the natural deduction system is complete for finite sequents, it suffices to show that every CNF tautology has a proof. But this is (almost) trivial. A CNF formula is a conjunction of clauses (disjunctions of literals). A conjunction is a tautology iff each of its conjuncts is a tautology, and by the rule ANDI, it is provable if each of its conjuncts is provable. A clause is tautologous iff it contains a pair of complementary literals such as p and NOTp, and any such clause is of the form (near enough, by the associativity and commutativity of disjunction) to something of the form  (p OR NOTp) OR A, which is easily proved by appending a step of ORI to an proof of the law of the excluded middle.

While the low-level details of the proof that C entails A₁ IMP (... IMP (A_n IMP B)) have not been exhibited explicitly, none of them are implausible and none present much difficulty, so with a small wave of the hands we declare this part of the proof done. However, the restriction to the finite case is a major limitation. Most valid sequents are infinite, so for the completeness theorem to be really interesting it must extend to sequents in which the premise set X contains infinitely many formulae.

What we need, therefore, is a demonstration that proving the finite sequents is enough. This is important enough to be designated a theorem in its own right.

Compactness Theorem:   Every valid sequent has a valid finite sub-sequent. That is, if  X STS A  then there is a finite subset X_fin of X such that  X_fin STS A. 

The argument for compactness proceeds by definition of a semantic tree. The language of propositional logic is built up with connectives out of an infinite supply of atoms  p₁, p₂, p₃, etc.  By an initial partial interpretation we mean an assignment of truth values 0 and 1 to the first n atoms  p₁, ..., p_n,  for some n. For example,

p₁: 1,   p₂: 0,   p₃: 0,   p₄: 1,  

is an initial partial interpretation for the case  n = 4. It consists in assigning 1 (true) to the atoms p₁ and p₄, while assigning 0 (false) to p₂ and p₃. Notice that it says nothing about assignments to the rest of the atoms, so it can be extended as we please by making more assignments, and in fact is consistent with absolutely any assignment to the atoms with subscripts above 4,

:   Nodes in the semantic tree Click for an animated version

The initial partial interpretations, ordered by the relation of set inclusion, form a tree, starting with the empty assignment as its root, in which each node consisting of an assignment to  p₁, ..., p_n.  has exactly two successors reached by asasigning 0 and 1 respectively to p_n+1. SemTree shows one node and its two successors. Let us refer to this entire semantic tree as 𝒯. We say that an assignment of values to the first n atoms is at level n in 𝒯. The above example is at level 4, for instance.

For simplicity, we may consider the set X as ordered in some way (say, by length of formulae and between formulae of the same length, by lexicographic order—the actual details don't matter as long as it is ordered somehow). Then we may define a subset of X, which we shall call X', as the result of removing all the redundant formulae from X, where a formula is "redundant" if it is logically equivalent to another formula which comes earlier in the order. A moment's thought should convince us that X and X' have exactly the same models, but X' has the nice property that, for every number n, it contains only finitely many formulae whose atoms are all among  p₁, ..., p_n,  because there are only finitely many truth functions of n variables. We call the subset of X' using just the first n atoms X'_n.

So  X' STS A  iff  X STS A . If X' is finite, we are home, so let's assume it is still infinite. We now suppose that no finite subset of X' entails A, and argue that, in that case, X' does not entail A either. To see this, consider the semantic tree 𝒯. We say that a node of 𝒯 is "dead" if the assignment of values it represents either makes some formula in X' false or makes A true. Otherwise it is "live". Since X'_n is finite, by hypothesis it does not entail A, so there is an assignment of values to its atoms and to those in A which makes all of its formulae true and A false. But all assignments to the atoms in the X'_n are nodes at level n (at most); consequently there must be at least one live node at every level of 𝒯.

The live nodes of 𝒯 form a sub-tree, since clearly if a node is live then so are all of its ancestors, right back to the root of the tree. This live sub-tree contains infinitely many nodes, since it contains at least one from each level of 𝒯, and 𝒯 has infinitely many levels. At each node it branches at most two ways, so all its forks are finite. But by König's lemma an infinite tree with finite forks must contain an infinite branch. Consider any such infinite branch: a path through 𝒯 consisting of live nodes, starting at the root and going on forever. Each step along its length adds a truth value for the next atom, so the whole branch represents an assignment of truth values to all atoms in the language. This assignment makes every formula in X' true and makes A false. Hence A is not a semantic consequence of X, and the result stands proved.

Originally published in 1927 (in German) Koenig, but it is essentially an easy observation which you can make for yourself.

So classical propositional entailment is compact. The main theorem that the natural deduction proof system is complete follows easily: if  X STS A  then by compactness there is a finite subset X_fin of X such that  X_fin STS A.  Since this sequent is finite, it can be turned into a single formula, which is a tautology iff the sequent is valid. All tautologies are theorems, and the steps needed to get back from the tautology to X_fin can be made into a derivation, so there is a proof of  X TS A  and natural deduction is complete.