The Interpolation Theorem

Definition of separation and inseparability

A sentence $!C$source separates sets of sentences $\Gamma$source and $\Delta$source if and only if $\Gamma \Entails !C$source and $\Delta \Entails \lnot !C$source. If no such sentence exists, then $\Gamma$source and $\Delta$source are inseparable.

Fresh constants preserve inseparability

Suppose $\Lang{L}_0$source is the language containing every constant symbol, function symbol and predicate symbol (other than $\doteq$source) that occurs in both $\Gamma$source and $\Delta$source, and let $\Lang{L}'_0$source be obtained by the addition of infinitely many new constant symbols $\Obj c_n$source for $n \ge 0$source. Then if $\Gamma$source and $\Delta$source are inseparable in $\Lang{L}_0$source, they are also inseparable in $\Lang{L}'_0$source.

Proof

We proceed indirectly: suppose by way of contradiction that $\Gamma$source and $\Delta$source are separated in $\Lang{L}'_0$source. Then $\Gamma \Entails \Subst{!C}{c}{x}$source and $\Delta \Entails \lnot \Subst{!C}{c}{x}$source for some $!C \in \Lang{L}_0$source (where $c$source is a new constant symbol---the case where $!C$source contains more than one such new constant symbol is similar). By compactness, there are finite subsets $\Gamma_0$source of $\Gamma$source and $\Delta_0$source of $\Delta$source such that $\Gamma_0 \Entails \Subst{!C}{c}{x}$source and $\Delta_0 \Entails \lnot \Subst{!C}{c}{x}$source. Let $!G$source be the conjunction of all formulas in $\Gamma_0$source and $!H$source the conjunction of all formulas in $\Delta_0$source. Then

From the former, by Generalization, we have $!G \Entails \lforall[x][!C]$source, and from the latter by contraposition, $\Subst{!C}{c}{x} \Entails \lnot !H$source, whence also $\lforall[x][!C] \Entails \lnot !H$source. Contraposition again gives $!H \Entails \lnot \lforall[x][!C]$source. By monotonicity,

so that $\lforall[x][!C]$source separates $\Gamma$source and $\Delta$source in $\Lang{L}_0$source.

Witness constants preserve inseparability

Suppose that $\Gamma \cup \{ \lexists[x][!S] \}$source and $\Delta$source are inseparable, and $c$source is a new constant symbol not in $\Gamma$source, $\Delta$source, or $!S$source. Then $\Gamma \cup \{ \lexists[x][!S], \Subst{!S}{c}{x} \}$source and $\Delta$source are also inseparable.

Proof

Suppose for contradiction that $!C$source separates $\Gamma \cup \{ \lexists[x][!S], \Subst{!S}{c}{x}\}$source and $\Delta$source, while at the same time $\Gamma \cup \{\lexists[x]{!S} \}$source and $\Delta$source are inseparable. We distinguish two cases:

1. $c$source does not occur in $!C$source: in this case $\Gamma \cup \{\lexists[x][!S], \lnot!C \}$source is satisfiable (otherwise $!C$source separates $\Gamma \cup \{\lexists[x][!S] \}$source and $\Delta$source). It remains so if $\Subst{!S}{c}{x}$source is added, so $!C$source does not separate $\Gamma \cup \{ \lexists[x][!S], \Subst{!S}{c}{x} \}$source and $\Delta$source after all.

2. $c$source does occur in $!C$source so that $!C$source has the form $\Subst{!C}{c}{x}$source. Then we have that

   $$\Gamma \cup \{ \lexists[x][!S], \Subst{!S}{c}{x}\} \Entails \Subst{!C}{c}{x},$$source

   whence $\Gamma, \lexists[x][!S] \Entails \lforall[x][(!S \lif !C)]$source by the Deduction Theorem and Generalization, and finally $\Gamma \cup \{ \lexists[x][!S] \} \Entails \lexists[x][!C]$source. On the other hand, $\Delta \Entails \lnot \Subst{!C}{c}{x}$source and hence by Generalization $\Delta \Entails \lnot \lexists[x][!C]$source. So $\Gamma \cup \{\lexists[x][!S] \}$source and $\Delta$source are separable, a contradiction.

Craig interpolation theorem

[Craig's Interpolation Theorem] If $\Entails !A \lif !B$source, then there is a sentence $!C$source such that $\Entails !A \lif !C$source and $\Entails !C \lif !B$source, and every constant symbol, function symbol, and predicate symbol (other than $\eq$source) in $!C$source occurs both in $!A$source and $!B$source. The sentence $!C$source is called an interpolant of $!A$source and $!B$source.

Proof

Suppose $\Lang{L}_1$source is the language of $!A$source and $\Lang{L}_2$source is the language of $!B$source. Let $\Lang{L}_0 = \Lang{L}_1 \cap \Lang{L}_2$source. For each $i \in \{0, 1, 2 \}$source, let $\Lang{L}'_i$source be obtained from $\Lang{L}_i$source by adding the infinitely many new constant symbols $\Obj c_0, \Obj c_1, \Obj c_2, \dots$source.

If $!A$source is unsatisfiable, $\lexists[x][\eq/[x][x]]$source is an interpolant. If $\lnot !B$source is unsatisfiable (and hence $!B$source is valid), $\lexists[x][\eq[x][x]]$source is an interpolant. So we may assume also that both $!A$source and $\lnot !B$source are satisfiable.

In order to prove the contrapositive of the Interpolation Theorem, assume that there is no interpolant for $!A$source and $!B$source. In other words, assume that $\{!A\}$source and $\{\lnot !B\}$source are inseparable in $\Lang{L}_0$source.

Our goal is to extend the pair $(\{ !A \}, \{\lnot!B\})$source to a maximally inseparable pair $(\Gamma^*, \Delta^*)$source. Let $!A_0$source, $!A_1$source, $!A_2$source, dots enumerate the sentences of $\Lang{L}_1$source, and $!B_0$source, $!B_1$source, $!B_2$source, dots enumerate the sentences of $\Lang{L}_2$source. We define two increasing sequences of sets of sentences $(\Gamma_n, \Delta_n)$source, for $n \ge 0$source, as follows. Put $\Gamma_0 = \{ !A\}$source and $\Delta_0 = \{\lnot !B \}$source. Assuming $(\Gamma_n, \Delta_n)$source are already defined, define $\Gamma_{n+1}$source and $\Delta_{n+1}$source by:

1. If $\Gamma_n \cup \{!A_n \}$source and $\Delta_n$source are inseparable in $\Lang{L}'_0$source, put $!A_n$source in $\Gamma_{n+1}$source. Moreover, if $!A_n$source is an existential formula $\lexists[x][!S]$source then pick a new constant symbol $c$source not occurring in $\Gamma_n$source, $\Delta_n$source, $!A_n$source or $!B_n$source, and put $\Subst{!S}{c}{x}$source in $\Gamma_{n+1}$source.

2. If $\Gamma_{n+1}$source and $\Delta_n \cup \{!B_n \}$source are inseparable in $\Lang{L}'_0$source, put $!B_n$source in $\Delta_{n+1}$source. Moreover, if $!B_n$source is an existential formula $\lexists[x][!S]$source, then pick a new constant symbol $c$source not occurring in $\Gamma_{n+1}$source, $\Delta_n$source, $!A_n$source or $!B_n$source, and put $\Subst{!S}{c}{x}$source in $\Delta_{n+1}$source.

Finally, define:

By simultaneous induction on $n$source we can now prove:

1. $\Gamma_n$source and $\Delta_n$source are inseparable in $\Lang{L}'_0$source;

2. $\Gamma_{n+1}$source and $\Delta_n$source are inseparable in $\Lang{L}'_0$source.

The basis for reference part-a is given by reference lem:sep1. For part reference part-b, we need to distinguish three cases:

1. If $\Gamma_0 \cup \{!A_0 \}$source and $\Delta_0$source are separable, then $\Gamma_1 = \Gamma_0$source and reference part-b is just reference part-a;

2. If $\Gamma_1 = \Gamma_0 \cup\{ !A_0\}$source, then $\Gamma_1$source and $\Delta_0$source are inseparable by construction.

3. It remains to consider the case where $!A_0$source is existential, so that $\Gamma_1 = \Gamma_0 \cup \{ \lexists[x][!S], \Subst{!S}{c}{x} \}$source. By construction, $\Gamma_0 \cup \{ \lexists[x][!S]\}$source and $\Delta_0$source are inseparable, so that by reference lem:sep2 also $\Gamma_0 \cup \{ \lexists[x][!S], \Subst{!S}{c}{x} \}$source and $\Delta_0$source are inseparable.

This completes the basis of the induction for reference part-a and reference part-b above. Now for the inductive step. For reference part-a, if $\Delta_{n+1} = \Delta_n \cup \{ !B_n \}$source then $\Gamma_{n+1}$source and $\Delta_{n+1}$source are inseparable by construction (even when $!B_n$source is existential, by reference lem:sep2); if $\Delta_{n+1} = \Delta_n$source (because $\Gamma_{n+1}$source and $\Delta_n \cup \{!B_n\}$source are separable), then we use the induction hypothesis on reference part-b. For the inductive step for reference part-b, if $\Gamma_{n+2} = \Gamma_{n+1} \cup \{!A_{n+1} \}$source then $\Gamma_{n+2}$source and $\Delta_{n+1}$source are inseparable by construction (even when $!A_{n+1}$source is existential, by reference lem:sep2); and if $\Gamma_{n+2} = \Gamma_{n+1}$source then we use the inductive case for reference part-a just proved. This concludes the induction on reference part-a and reference part-b.

It follows that $\Gamma^*$source and $\Delta^*$source are inseparable; if not, by compactness, there is $n \ge 0$source that separates $\Gamma_n$source and $\Delta_n$source, against reference part-a. In particular, $\Gamma^*$source and $\Delta^*$source are consistent: for if the former or the latter is inconsistent, then they are separated by $\lexists[x][\eq/[x][x]]$source or $\lforall[x][\eq[x][x]]$source, respectively.

We now show that $\Gamma^*$source is maximally consistent in $\Lang{L}'_1$source and likewise $\Delta^*$source in $\Lang{L}'_2$source. For the former, suppose that $!A_n \notin \Gamma^*$source and $\lnot !A_n \notin \Gamma^*$source, for some $n \ge 0$source. If $!A_n \notin \Gamma^*$source then $\Gamma_n \cup \{!A_n \}$source is separable from $\Delta_n$source, and so there is $!C \in \Lang{L}'_0$source such that both:

Likewise, if $\lnot !A_n \notin \Gamma^*$source, there is $!C' \in \Lang{L}'_0$source such that both:

By propositional logic, $\Gamma^* \Entails !C \lor !C'$source and $\Delta^* \Entails \lnot (!C \lor !C')$source, so $!C \lor !C'$source separates $\Gamma^*$sourceand $\Delta^*$source. A similar argument establishes that $\Delta^*$source is maximal.

Finally, we show that $\Gamma^* \cap \Delta^*$source is maximally consistent in $\Lang{L}'_0$source. It is obviously consistent, since it is the intersection of consistent sets. To show maximality, let $!S \in \Lang{L}'_0$source. Now, $\Gamma^*$source is maximal in $\Lang{L'_1} \supseteq \Lang{L'_0}$source, and similarly $\Delta^*$source is maximal in $\Lang{L'_2} \supseteq \Lang{L'_0}$source. It follows that either $!S \in \Gamma^*$source or $\lnot !S \in \Gamma^*$source, and either $!S \in \Delta^*$source or $\lnot !S \in \Delta^*$source. If $!S \in \Gamma^*$source and $\lnot !S \in \Delta^*$source then $!S$source would separate $\Gamma^*$source and $\Delta^*$source; and if $\lnot !S \in \Gamma^*$source and $!S \in \Delta^*$source then $\Gamma^*$source and $\Delta^*$source would be separated by $\lnot !S$source. Hence, either $!S \in \Gamma^* \cap \Delta^*$source or $\lnot !S \in \Gamma^* \cap \Delta^*$source, and $\Gamma^* \cap \Delta^*$source is maximal.

Since $\Gamma^*$source is maximally consistent, it has a model $\Struct{M}'_1$source whose domain $\Domain{M'_1}$source comprises all and only the elements $\Assign{c}{M'_1}$source interpreting the constant symbols---just like in the proof of the completeness theorem (reference thm:completeness). Similarly, $\Delta^*$source has a model $\Struct{M}'_2$source whose domain $\Domain{M'_2}$source is given by the interpretations $\Assign{c}{M'_2}$source of the constant symbols.

Let $\Struct{M_1}$source be obtained from $\Struct{M'_1}$source by dropping interpretations for constant symbols, function symbols, and predicate symbols in $\Lang{L'_1} \setminus \Lang{L'_0}$source, and similarly for $\Struct{M_2}$source. Then the map $h \colon M_1 \to M_2$source defined by $h(\Assign{c}{M'_1}) = \Assign{c}{M'_2}$source is an isomorphism in $\Lang{L}'_0$source, because $\Gamma^* \cap \Delta^*$source is maximally consistent in $\Lang{L}'_0$source, as shown. This follows because any $\Lang{L}'_0$source-sentence either belongs to both $\Gamma^*$source and $\Delta^*$source, or to neither: so $\Assign{c}{M'_1} \in \Assign{P}{M'_1}$source if and only if $\Atom{P}{c} \in \Gamma^*$source if and only if $\Atom{P}{c} \in \Delta^*$source if and only if $\Assign{c}{M'_2} \in \Assign{P}{M'_2}$source. The other conditions satisfied by isomorphisms can be established similarly.

Let us now define a model $\Struct{M}$source for the language $\Lang{L_1} \cup \Lang{L_2}$source as follows:

1. The domain $\Domain{M}$source is just $\Domain{M_2}$source, i.e., the set of all elements $\Assign{c}{M'_2}$source;

2. If a predicate symbol $P$source is in $\Lang{L_2} \setminus \Lang{L_1}$source then $\Assign{P}{M} = \Assign{P}{M'_2}$source;

3. If a predicate $P$source is in $\Lang{L}_1\setminus \Lang{L}_2$source then $\Assign{P}{M} = h(\Assign{P}{M'_1})$source, i.e., $\tuple{\Assign{c_1}{M'_2}, \dots, \Assign{c_n}{M'_2}} \in \Assign{P}{M}$source if and only if $\tuple{\Assign{c_1}{M'_1}, \dots, \Assign{c_n}{M'_1}} \in \Assign{P}{M'_1}$source.

4. If a predicate symbol $P$source is in $\Lang{L}_0$source then $\Assign{P}{M} = \Assign{P}{M'_2} = h(\Assign{P}{M'_1})$source.

5. Function symbols of $\Lang{L}_1 \cup \Lang{L}_2$source, including constant symbols, are handled similarly.

Finally, one shows by induction on formulas that $\Struct{M}$source agrees with $\Struct{M'_1}$source on all formulas of $\Lang{L'_1}$source and with $\Struct{M'_2}$source on all formulas of $\Lang{L'_2}$source. In particular, $\Struct{M} \Entails \Gamma^* \cup \Delta^*$source, whence $\Struct{M} \Entails !A$source and $\Struct{M} \Entails \lnot!B$source, and $\not\Entails !A \lif !B$source. This concludes the proof of Craig's Interpolation Theorem.

Definition of explicit definability

Suppose $\Lang{L}$source is a language not containing the predicate symbol $P$source. A set $\Sigma(P)$source of sentences of $\Lang{L} \cup \{P\}$source explicitly defines $P$source if and only if there is a formula $!C(x_1, \dots, x_n)$source of $\Lang{L}$source such that

Definition of implicit definability

Suppose $\Lang{L}$source is a language not containing the predicate symbols $P$source and $P'$source. A set $\Sigma(P)$source of sentences of $\Lang{L} \cup \{P\}$source implicitly defines $P$source if and only if

where $\Sigma(P')$source is the result of uniformly replacing $P$source with $P'$source in $\Sigma(P)$source.

Beth definability theorem

[Beth Definability Theorem] A set $\Sigma(P)$source of $\Lang{L} \cup\{P\}$source-formulas implicitly defines $P$source if and only $\Sigma(P)$source explicitly defines $P$source.

Proof

If $\Sigma(P)$source explicitly defines $P$source then both

and the conclusion follows. For the converse: assume that $\Sigma(P)$source implicitly defines $P$source. First, we add constant symbols $c_1$source, dots, $c_n$source to $\Lang{L}$source. Then

By compactness, there are finite sets $\Delta_0 \subseteq \Sigma(P)$source and $\Delta_1 \subseteq \Sigma(P')$source such that

Let $!D(P)$source be the conjunction of all sentences $!A(P)$source such that either $!A(P) \in \Delta_0$source or $!A(P') \in \Delta_1$source and let $!D(P')$source be the conjunction of all sentences $!A(P')$source such that either $!A(P) \in \Delta_0$source or $!A(P') \in \Delta_1$source. Then $!D(P) \land !D(P') \Entails \Atom{P}{c_1, \dots, c_n} \to \Atom{P'}{c_1, \dots, c_n}$source. We can re-arrange this so that each predicate symbol occurs on one side of $\Entails$source:

By Craig's Interpolation Theorem there is a sentence $!C(c_1,\dots, c_n)$source not containing $P$source or $P'$source such that:

From the former of these two entailments we have: $!D(P) \Entails \Atom{P}{c_1,\dots, c_n} \lif !C(c_1,\dots, c_n)$source. And from the latter, since an $\Lang{L} \cup \{P\}$source-model $\Expan{M}{R} \Entails !A(P)$source if and only if the corresponding $\Lang{L} \cup \{P'\}$source-model $\Expan{M}{R} \models !A(P')$source, we have $!C(c_1,\dots, c_n) \Entails !D(P) \lif \Atom{P}{c_1,\dots, c_n}$source, from which:

Putting the two together, $!D(P) \Entails \Atom{P}{c_1,\dots, c_n} \liff !C(c_1, \dots, c_n)$source, and by monotonicity and generalization also