First order completeness Metalogic
The last four sections have covered several proofs of the completeness of natural deduction for propositional logic as defined by truth-functional semantics. In order to obtain a similar result at the full first order level, we need a more elaborate construction because the language is so much richer; the interpretation function has to apply to names, predicate symbols and whatever function symbols may be present, and then we have to be concerned with m-variants of interpretations and so forth. It may be worth re-reading the section on the semantics of quantifiers as a reminder of the setting.
Let us begin by simplifying the problem a little by restricting it to the case in which the conclusion of the sequent of interest is the absurd constant BAD. As already noted, we lose no generality by doing this, since an arbitrary sequent X TS A can be recovered in a couple of steps of natural deduction from X, NOTA TS BAD which is of the restricted form and which is valid if X STS A. While we are framing the problem, let us fix vocabulary, by saying that a set X of formulae is consistent iff there is no derivation of BAD from it, and that it is satisfiable iff there is an interpretation for which all formulae in it are true. That is, consistency is a purely deduction-theoretic notion, while satisfiability is a purely semantic one. In these terms, then, the present challenge is to show that every unsatisfiable set is inconsistent, or to put it the other way around, that every consistent set is satisfiable.
The last of our proofs of completeness for the propositional case is the one which we shall adapt for this purpose. It is best seen as proceeding via two lemmas: every consistent set has a maximal consistent superset, and every maximal consistent set has a model. These lemmas are true for quantified logic as well, but have to be formulated carefully and need extra steps for their proof.
A first order language is determined by the set of predicate and function symbols (including names) which it incorporates. Such a language can always be extended by the addition of more symbols, to give a bigger language in which some more things can be said. When we say that a set is consistent, we should be careful to specify that it is consistent in a given language, meaning that there is no derivation in that language of a contradiction from it. In larger languges, of course, there will be more derivations from it, so there is a threat that a set which is consisent in one language could be inconsistent in another, if one of these extra derivations going through the additional vocabulary were somehow to reach a contradiction which was unreachable before. The first real step in the proof is to note that this never happens.
Language extension lemma: Where £ is a first order language with function symbols ℱ, and £' is an extended language differing only in that it has infinitely many names (0-ary function symbols) which are not in ℱ, any set X of formulae which is consistent in £ is also consistent in £'.
Suppose X is inconsistent in £'. Consider any derivation of BAD from X in the extended language. Since all derivations are finite, at most finitely many of the old names and finitely many of the new ones occur in it. Nothing turns on the spelling of the new names, and there are infinitely many unused old ones available in £, so the derivation could equally well have used some of the previously unused names from £ in place of the new ones (as they are all just undefined symbols foreign to the entire proof, so the choice between them does not affect the operation of any inference steps). Therefore X was already inconsistent in £.
Another way to think of £' is simply as a re-branding of £. The names in £ can be enumerated as a1, a2, a3, etc. Obviously, the subscripts do not carry any semantic weight—they are just part of the spelling—so nothing essentially changes if we double them all and write the existing names as a2, a4, a6, etc. The effect is that everything (proofs, etc.) in £ is now re-written to be in the fragment of £ with no odd-numbered names, but this is a difference of no real substance. The new names can then be added, with the spelling convention that they have odd-numbered subscripts, and we thus have all of £ back again, but with everything interesting confined to the even-numbered part of it, and the "new" names added but doing nothing. On that reading, the derivation in £' already is a derivation in £.
We have seen in the proof of completeness for the propositional case that maximal consistent sets play nicely with the connectives, in the sense that the conditions under which formulae are members of such a set exactly follow the truth tables for their main connectives. Quantifiers, however, are different. What we would like, in order to construct an interpretation out of the maximal consistent set Σ, is that a universal claim ALLvA is in Σ just when all of its instances Atv are, and dually an existential SOMEvA is in Σ iff at least one instance Atv is also in Σ. That at least gives us a chance that interpreting the term t might provide a member of the domain serving to define the m-variant needed for the semantics of the quantifier. Unfortunately, however, there is no reason why a maximal consistent set should have any such property (indeed, most of them don't) so we need to do some more work.
Let us say that a term t is a trigger for ALLvA over a class of interpretations if the conditional Atv IMP ALLvA is true for all interepretations in the class. If a universal formula has a trigger, therefore, and all of its instances are true for a particular interpretation, then the trigger will be among the true instances and the universal will follow. In a similar way, we shall say that t is a witness for an existential formula SOMEvA over a class of interpretations if the conditional SOMEvA IMP Atv is true for all of those interepretations. An existential with a witness cannot be barely true for one of those interpretations: if it is true that there is something satisfying A then there has to be an actual example of such a thing, named by an actual term t.
Since the theorems provable in the natural deduction system are all derivable from X (as indeed they are from any assumptions), we may look to them to provide terms t to witness or trigger the claims made by quantified formulae as desired. In particular, we note a pair of remarkable theorems peculiar to classical logic:
In completeness proofs for non-classical logics, this short cut is unavailable, so securing witnesses for the existential claims tends to be more difficult, though the underlying idea of constructing the range of variables somehow out of terms in the language is fairly general.| TS SOMEx(Fx IMP ALLyFy) | Click to see the proof | Do it yourself | ||
| TS SOMEx(SOMEyFy IMP Fx) | Click to see the proof | Do it yourself |
The first of these (almost) says that every universal formula has a trigger, and the second (almost) says that every existential one has a witness. The proof now proceeds by spelling out these claims literally, constructing our target maximal consistent set in such a way as effectively to remove the word "almost" from these observations.
Let us say that the language in which the set X is expressed is £. Now, in order to supply triggers and witnesses, add an infinite supply of new names or "constants". We may think of these as arranged in a 2-dimensional array, with infinitely many rows and infinitely many columns:
| a1,1 | a1,2 | a1,3 | ... |
| a2,1 | a2,2 | a2,3 | ... |
| a3,1 | a3,2 | a3,3 | ... |
| etc |
Witness lemma: X* is consistent in £*
Proof of this is by appeal to SOMEE. Suppose for the sake of contradiction that there is a derivation of BAD from X*. The last line of such a derivation must have BAD as its formula, and its assumptions are members of X together with finitely many formulae from 𝒲*. Each of these latter must be of the form SOMEvA IMP Acv. The name c does not occur in any other assumption, as it is foreign to £ and by construction all the witnesses are distinct. Hence we can append a proof of the theorem TS SOMEx(SOMEvA IMP Ax )v and apply SOMEE to this to remove SOMEvA IMP Acv from the set of assumptions. Repeating as often as required removes all assumptions which come from 𝒲*, leaving a derivation of BAD from X. But by hypothesis X is consistent, so there can be no such derivation. Therefore the original supposition must be wrong: there is no derivation of BAD from X*.
Lindenbaum's lemma: X* has a maximal consistent superset Σ in the language £*.
Proof is by the same construction as was applied in the propositional case, and does not need to be repeated here.
As before, Σ is closed under natural deduction and respects the truth tables (contains NOTA iff it does not contain A, contains A AND B iff it contains A and contains B, etc). Since it inherits all the witnesses and triggers from X*, it is also saturated (contains an existential formula iff it contains an instance) and rich (contains a universal formula iff it contains all instances). All that is needed, therefore, to turn it into the basis for an interpretation is a suitable domain and suitable definitions of the function and predicate symbols.
The easiest way to achieve that is to turn the language on itself! By the Herbrand universe of a first order language we mean the set of terms (i.e. ground terms, excluding variables) of the language. This is certainly a non-empty set, and so can form the domain of an interpretation which we shall call H. Interpreting the function symbols of £* over this domain is particularly simple: following Herbrand, we observe that every function symbol can be interpreted as itself! Where m is a name, we require H(m) to be a member of the domain—but m itself is a member of the domain, so we stipulate that H(m) = m. An n-ary function symbol f, as an expression in the language, applies to n terms t1, ..., tn to form a new term f(t1, ..., tn). Those terms are all objects in the Herbrand domain, so we may simply stipulate that H(f) = f. This has the effect that every term of the language denotes itself: δ(t) = t for every term t in the language. Herbrand's construction is gloriously simple, and the most beautiful feature is that it works!
Jacques Herbrand (1908–1931), the French mathematician who introduced this construction as a way of devising models of first order theories. Although he died at the age of only 23, his contribution to the metatheory of logic remains fundamental.To complete H as an interpretation, we must define H(F) for each predicate symbol F. Well, the value assigned to n-ary predicate symbol F needs to be a set of n-tuples of elements of the domain. The domain consists of terms of the language, so naturally we take H(F) to be the set of n-tuples <t1, ..., tn> such that the atomic formula Ft1...tn is in Σ. Unsurprisingly, this forces H to agree with Σ about atoms: any atomic formula is true for H iff it is in Σ, because H was defined that way.
To complete the story, then, we observe that, in virtue of the facts that Σ is maximal consistent, saturated and rich, the correspondence between truth for H and membership of Σ extends from the atomic case up to all formulae. The argument is by cases, one for each connective and quantifier. The cases of the connectives are as for propositional logic, so only the quantifiers need comment. Consider a formula SOMEvA and let m be a name which does not occur in it. Suppose SOMEvA is true for H. What that means is that there is some m-variant of H for which Amv is true. Let it be H[m←t]. What m denotes in H[m←t] is what t denotes in H, so the value of Amv in H[m←t] is the same as the value of Atv in H. That is to say Atv is true for H, and since it is shorter than SOMEvA we are entitled to assume it is in Σ. Since Σ is closed under the natural deduction rules, it follows by SOMEI that SOMEvA is in Σ. Conversely, suppose that SOMEvA is in Σ. Σ contains a witness formula SOMEvA IMP Acvso Acv is in Σ, and therefore true for H. Therefore Amv is true for H[m←c], so SOMEvA is true for H.
In sum, every formula in X* is true for H. X is a subset of X*, so X is satisfiable as required.