264 THE CRAIG INTERPOLATION THEOREM

20.2 Robinson’s Joint Consistency Theorem

We begin with a preliminary result.

20.5 Lemma. The union T1 T2 of two theories T1 and T2 is satisfiable if and only if there is no sentence in T1 whose negation is in T2.

Proof: The ‘only if’ part is obvious: if there were a sentence in T1 whose negation was T2, the union could not possibly be satisfiable; for there could be no interpretation in which both the sentence and its negation were true.

The ‘if’ part follows quickly from the compactness theorem and Craig’s theorem: Suppose the union of T1 and T2 is unsatisfiable. Then by the compactness theorem, there is a finite subset S0 of the union which is unsatisfiable. If there are no members of S0 that belong to T1, then T2 is unsatisfiable, and so x x = x is a sentence in T1 whose negation is in T2; if no members of S0 belong to T2, then T1 is unsatisfiable, and so x x = x is a sentence in T1 whose negation is in T2. So we may suppose that S0 contains some members both of T1 and of T2. Let F1, . . . , Fm be the members of S0 that are in T1; let G1, . . . , Gn be the members of S0 that are in T2.

Let A be (F1 & . . . & Fm ), and let C be (G1 & . . . & Gn ). A implies C. By Craig’s theorem, there is a sentence B implied by A, implying C, and containing only nonlogical symbols contained in both A and C. B is therefore a sentence in the languages of both T1 and T2. Since A is in T1 and implies B, B is in T1. Since (G1 & . . . & Gn ) is in T2, so is B, as (G1 & . . . & Gn ) implies B. So B is a sentence in T1 whose negation is in T2.

An extension T of a theory T is just another theory containing it. The extension is called conservative if every sentence of the language of T that is a theorem of T is a theorem of T . We next prove a theorem about conservative extensions.

20.6 Theorem. Let L0, L1, L2 be languages, with L0 = L1 ∩ L2. Let Ti be a theory in Li for i = 0, 1, 2. Let T3 be the set of sentences of L1 L2 that are consequences of T1 T2. Then if T1 and T2 are both conservative extensions of T0, then T3 is also a conservative extension of T0.

Proof: Suppose B is a sentence of L0 that is a theorem of T3. We must show that B is a theorem of T0. Let U2 be the set of sentences of L2 that are consequences of T2 {B}. Since B is a theorem of T3, T1 T2 {B} is unsatisfiable, and therefore T1 U2 is unsatisfiable. Therefore there is a sentence D in T1 whose negation D is in U2. D is a sentence of L1, and D of L2. Thus D and D are both in L0, and hence so is ( B → D). Since D is in T1, which is a conservative extension of T0, D is in T0. And since D is in U2, ( B → D) is in T2, which is a conservative extension of T0. Thus ( B → D) is also in T0, and therefore so is B, which follows from D and ( B → D).

An immediate consequence is

20.7 Corollary (Robinson’s joint consistency theorem). Let L0, L1, L2 be languages, with L0 = L1 ∩ L2. Let Ti be a theory in Li for i = 0, 1, 2. If T0 is complete, and T1 and T2 are satisfiable extensions of T0, then T1 T2 is satisfiable.

Proof: A satisfiable extension of a complete theory is conservative, and a conservative extension of a satisfiable theory is satisfiable. Thus if the Ti satisfy the hypotheses of Corollary 20.7, then T3 as defined in Theorem 20.6 is a satisfiable extension of T0, and therefore T1 T2 is satisfiable.

20.8 Example (Failures of joint consistency). Let L0 = L1 = L2 = { P, Q}, where P and Q are one-place predicates. Let T1 (respectively, T2) be the set of consequences in L1 (respectively, L2) of { x P x, x Qx} (respectively, { x P x, x Qx}. Let T0 be the set of consequences in L0 of x P x. Then T1 T2 is not satisfiable, though each of T1 and T2 is a satisfiable extension of T0. This is not a counterexample to Robinson’s theorem, because T0 is not complete. If instead we let L0 = { P}, then again we do not get a counterexample, because then L0 is not the intersection of L1 and L2, while L is. This shows the hypotheses in Corollary 20.7 are needed.

We have proved Robinson’s theorem using Craig’s theorem. Robinson’s theorem can also be proved a different way, not using Craig’s theorem, and then used to prove Craig’s theorem. Let us indicate how a ‘double compactness’ argument yields Craig’s theorem from Robinson’s.

Suppose A implies C. Let L1 (L2) be the language consisting of the nonlogical symbols occurring in A (C). Let L0 = L1 ∩ L2. We want to show there is a sentence B of L0 implied by A and implying C. Let be the set of sentences of L0 that are implied by A. We first show that {C} is unsatisfiable. Suppose that it is not and that Mis a model of {C}. Let T0 be the set of sentences of L0 that are true in M. T0 is a complete theory whose langauge is L0. Let T1 (T2) be the set of sentences of L1 (L2) that are consequences of T0 { A} (T0 {C}). T2 is a satisfiable extension of T0: Mis a model of T0 {C}, and hence of T2. But T1 T2 is not satisfiable: any model of T1 T2 would be a model of { A, C}, and since A implies C, there is no such model. Thus by the joint consistency theorem, T1 is not a satisfiable extension of T0, and therefore T0 { A} is unsatisfiable. By the compactness theorem, there is a finite set of sentences in T0 whose conjunction D, which is in L0, implies A. Thus A implies D, D is in L0, D is in , and D is therefore true in M. But this is a contradiction, as all of the conjuncts of D are in T0 and are therefore true in M. So{C} is unsatisfiable, and by the compactness theorem again, there is a finite set of members of whose conjunction B implies C. B is in L0, since its conjuncts are, and as A implies each of these, A implies B.

20.3 Beth’s Definability Theorem

Beth’s definability theorem is a result about the relation between two different explications, or ways of making precise, the notion of a theory’s giving a definition of one concept in terms of other concepts. As one might expect, each of the explications discusses a relation that may or may not hold between a theory, a symbol in the language of that theory (which is supposed to ‘represent’ a certain concept), and other symbols in the language of the theory (which ‘represent’ other concepts), rather than directly discussing a relation that may or may not hold between a theory, a concept,

and other concepts. The supposition of Beth’s theorem, then, is that α and β1, . . . , βn are nonlogical symbols of the language L of some theory T and that α is not among the βi .

The first explication is straightforward and embodies the idea that a theory defines a concept in terms of others when ‘a definition of that concept in terms of the others is a consequence of the theory’. This sort of definition is called an explicit definition: we say that α is explicitly definable in terms of the βi in T if a definition of α from the βi is one of the sentences in T. What precisely is meant by a definition of α in terms of the βi depends on whether α is a predicate or a function symbol. In the case of a (k + 1)-place predicate, such a definition is a sentence of the form

x0 x1 · · · xk (α(x0, x1, . . . , xk ) ↔ B(x0, . . . , xk ))

and in case of a k-place function symbol, such a definition is a sentence of the form

x0 x1 · · · xk (x0 = α(x1, . . . , xk ) ↔ B(x0, . . . , xk ))

where in either case B is a formula whose only nonlogical symbols are among the βi . (Constants may be regarded as 0-place function symbols, and do not require separate discussion. In this case the right side of the biconditional would simply be x0 = α.) The general form of a definition may be represented as

x0 · · · xk (—α, x0, . . . , xk — ↔ B(x0, . . . , xk )).

The second explication is rather more subtle, and incorporates the idea that a theory defines a concept in terms of others if ‘any specification of the universe of discourse of the theory and the meanings of the symbols representing the other concepts (that is compatible with the truth of all the sentences in the theory) uniquely determines the meaning of the symbol representing that concept’. This sort of definition is called implicit definition: we say that α is implicitly definable from the βi in T if any two models of T that have the same domain and agree in what they assign to the βi also agree in what they assign to α.

It will be useful to develop a more ‘syntactic’ reformulation of this ‘semantic’ definition of implicit definability. To this end, we introduce a new language L obtained from L by replacing every nonlogical symbol γ of L, other than the βi , by a new symbol γ of the same kind: 17-place function symbols are replaced by 17-place function symbols, 59-place predicates by 59-place predicates, and so on.

Given two models M and N of T that have the same domain and agree on what they assign to the βi , we let M+ N be the interpretation of L L that has the same domain, and assigns the same denotations to the βi , and, for any other nonlogical symbol γ of L, assigns to γ what M assigns to γ , and assigns to γ what N assigns to γ . Then M+ N is a model of T T .

Conversely, if K is a model of T T , then K can clearly be ‘decomposed’ into two models M and N of T , which have the same domain (as each other, and as K) and agree (with each other and with K) on what they assign to the βi , where for any other nonlogical symbol γ of L, what M assigns to γ is what K assigns to γ , and what N assigns to γ is what K assigns to γ .

Proof: Here, of course, by —α , x0, . . . , xk — is meant the result of substituting α for α in —α, x0, . . . , xk —. Note that (1) will be true in a given interpretation if and only if that interpretation assigns the same denotation to α and to α .

For the left-to-right direction, suppose α is implicitly definable from the βi in T . Suppose K is a model of T T . Let M and N be the models into which K can be decomposed as above, so that K = M + N . Then M and N have the same domain and agree on what they assign to the βi . By the supposition of implicit definability, they must therefore agree on what they assign to α. Therefore the biconditional (1) is true in K. In other words, any model of T T is a model of (1), which therefore is a consequence of T T .

For the right-to-left direction, suppose that (1) follows from T T . Suppose M and N are models of T that have the same domain and agree on what they assign to the βi . Then M+ N is a model of T T and therefore of (1), by the supposition that

(1) is a consequence of T T . It follows that M+ N assigns the same denotation to α and α , and therefore that M and N assign the same denotation to α. Thus α is implicitly definable from the βi in T .

One direction of the connection between implicit and explicit definability is now easy.

20.10 Proposition (Padoa’s method). If α is not implicitly definable from the βi in T , then α is not explicitly definable from the βi in T .

Proof: Suppose α is explicitly definable from the βi in T . Then some definition

is in T . (Recall that B involves only the βi , which are not replaced by new nonlogical symbols.) Since (1) of Lemma 20.9 is a logical consequence of (2) and (3), it is a consequences of T T , and by that lemma, α is implicitly definable from the βi in T .

20.11 Theorem (Beth’s definability theorem). α is implicitly definable from the βi in T if and only if α is explicitly definable from the βi in T .

Proof: The ‘if’ direction is the preceding proposition, so it only remains to prove the ‘only if’ direction. So suppose α is implicitly definable from the βi in T. Then

(1) of Lemma 20.9 is a consequence of T T . By the compactness theorem, it is a consequence of some finite subset of T T . By adding finitely many extra sentences to it, if necessary, we can regard this finite subset as T0 T0 , where T0 is a finite subset of T , and T0 comes from T0 on replacing each nonlogical symbol γ other than the βi