First-Order Interpolation of Non-classical Logics Derived from Propositional Interpolation

Abstract

This paper develops a general methodology to connect propositional and first-order interpolation. In fact, the existence of suitable skolemizations and of Herbrand expansions together with a propositional interpolant suffice to construct a first-order interpolant. This methodology is realized for lattice-based finitely-valued logics, the top element representing true and for (fragments of) infinitely-valued first-order Gödel logic, the logic of all linearly ordered constant domain Kripke frames.

1 Introduction

Ever since Craig’s seminal result on interpolation [8], interpolation properties have been recognized as important desiderata of logical systems. Craig interpolation has many applications in mathematics and computer science, for instance consistency proofs, model checking [18], proofs in modular specifications and modular ontologies. Recall that a logic L has interpolation if whenever $A \supset B$ holds in L there exists a formula I in the common language of A and B such that $A \supset I$ and $I \supset B$ both hold in L.

Propositional interpolation properties can be determined and classified with relative ease using the ground-breaking results of Maksimova cf. [12,13,14]. This approach is based on an algebraic analysis of the logic in question. In contrast first-order interpolation properties are notoriously hard to determine, even for logics where propositional interpolation is more or less obvious. For example it is unknown whether $\mathrm{G}_{[0,1]}^\mathrm{QF}$ (first-order infinitely-valued Gödel logic) interpolates (cf [1]) and even for $\mathrm{MC}^\mathrm{QF}$, the logic of constant domain Kripke frames of 3 worlds with 2 top worlds (an extension of MC), interpolation proofs are very hard cf. Ono [17]. This situation is due to the lack of an adequate algebraization of non-classical first-order logics.

In this paper we present a proof theoretic methodology to reduce first-order interpolation to propositional interpolation:

$$\begin{aligned} \left. \begin{array}{r} \text{ existence } \text{ of } \text{ suitable } \text{ skolemizations } + \\ \text{ existence } \text{ of } \text{ Herbrand } \text{ expansions } + \\ \text{ propositional } \text{ interpolance } \, \, \, \, \end{array} \right\} \rightarrow \begin{array}{c} \text{ first-order }\\ \text{ interpolation. }\end{array} \end{aligned}$$

The construction of the first-order interpolant from the propositional interpolant follows this procedure:

• 1. Develop a validity equivalent skolemization replacing all strong quantifiers (negative existential or positive universal quantifiers) in the valid formula $A \supset B$ to obtain the valid formula $A_1 \supset B_1$.

• 2. Construct a valid Herbrand expansion $A_2 \supset B_2$ for $A_1 \supset B_1$. Occurrences of $\exists x B(x)$ and $\forall x A(x)$ are replaced by suitable finite disjunctions $\bigvee B(t_i )$ and conjunctions $\bigwedge B(t_i)$, respectively.

• 3. Interpolate the propositionally valid formula $A_2 \supset B_2$ with the propositional interpolant $I^{*}$:

  $$\begin{aligned} A_2 \supset I^* \quad \text{ and } \quad I^* \supset B_2 \end{aligned}$$

  are propositionally valid.

• 4. Reintroduce weak quantifiers to obtain valid formulas

  $$\begin{aligned} A_1 \supset I^* \quad \text{ and } \quad I^* \supset B_1 . \end{aligned}$$

• 5. Eliminate all function symbols and constants not in the common language of $A_1$ and $B_1$ by introducing suitable quantifiers in $I^*$ (note that no Skolem functions are in the common language, therefore they are eliminated). Let I be the result.

• 6. I is an interpolant for $A_1 \supset B_1$. $A_1 \supset I$ and $I \supset B_1$ are skolemizations of $A \supset I$ and $I \supset B$. Therefore I is an interpolant of $A \supset B$.

We apply this methodology to lattice based finitely-valued logics and the weak quantifier and subprenex fragments of infinitely-valued first-order Gödel logic.

Note that finitely-valued first-order logics admit variants of Maehara’s Lemma and therefore interpolate if all truth values are quantifier free definable [16]. For logics where not all truth-values are represented by quantifier-free formulas this argument does not hold, which explains the necessity of different interpolation arguments for e.g. $\mathrm{MC}^\mathrm{QF}$ (the result for $\mathrm{MC}^\mathrm{QF}$ is covered by our framework, cf. Example 2).

2 Lattice-Based Finitely-Valued Logics

We consider finite lattices $L = \langle W, \le , \cup , \cap , 0, 1 \rangle$ where $\cup , \cap , 0, 1$ are supremum, infimum, minimal element, maximal element and $0 \not = 1$, [7].

Definition 1

A propositional language for L, $\mathcal {L}^{0}(L,V)$, $V \subseteq W$ is based on propositional variables $x_n$, $n \in$ N, truth constants $C_v$ for $v \in V$, $\vee$, $\wedge$, $\supset$.

Definition 2

A first-order language for L, $\mathcal {L}^{1}(L,V)$, $V \subseteq W$ is based on the usual first-order atoms, truth constants $C_v$ for $v \in V$, $\vee , \wedge , \supset , \exists , \forall$.

We write $\bot$ for $C_0$, $\top$ for $C_1$, $\lnot A$ for $A \supset \bot$ if $0 \in V$.

Definition 3

$\rightarrow : W \times W \Rightarrow W$ for $L = \langle W, \le , \cup , \cap , 0, 1 \rangle$ is an admissible implication iff

$$\begin{aligned} u \rightarrow v = 1 \quad \text{ iff } \quad u \le v, \end{aligned}$$

$$\begin{aligned} \text{ if } \quad u \le v, f \le g \quad \text{ then } \quad v \rightarrow f \le u \rightarrow g. \end{aligned}$$

Definition 4

The propositional logic $\mathbf{L }^{0}(L,V,\rightarrow )$ based on $\mathcal {L}^{0}(L,V)$, L $=$ $\langle$ $W, \le , \cup , \cap , 0, 1$ $\rangle$, $\rightarrow$ an admissible implication is defined as follows: $\varPhi ^0$ is a propositional valuation iff

• 1. $\varPhi ^{0}(x) \in W$ for a propositional variable x,

• 2. $\varPhi ^{0}(C_v ) = v$,

• 3. $\varPhi ^{0}(A \vee B) = \varPhi ^{0}(A) \cup \varPhi ^{0}(B)$,

• 4. $\varPhi ^{0}(A \wedge B) = \varPhi ^{0}(A) \cap \varPhi ^{0}(B)$,

• 5. $\varPhi ^{0}(A \supset B) = \varPhi ^{0}(A) \rightarrow \varPhi ^{0}(B)$.

$$\begin{aligned} \models ^0 A \text{ iff } \forall \varPhi ^{0}: \varPhi ^{0}(A) = 1 \quad \text{ L }(L,V, \rightarrow ) = \{A \, | \, \models ^0 A\} \end{aligned}$$

we write $A_1 \ldots A_n \models ^0 B$ iff for all $\varPhi ^0$ $\varPhi ^0 (A_1 ) = 1 \text{ and } \ldots \text{ and } \varPhi ^0 (A_n ) = 1$ implies $\varPhi ^0 (B) = 1$.

Definition 5

The first-order logic $\mathbf{L }^{1}(L,V,\rightarrow )$ based on $\mathcal {L}^{1}(L, V)$, $L = \langle W, \le , \cup ,\cap , 0, 1 \rangle$, $\rightarrow$ an admissible implication is defined as follows: $\varPhi ^{1}$ is a first-order valuation into a structure $\langle D_{\varPhi ^{1}}, \varOmega _{\varPhi ^{1}} \rangle$, $D_{\varPhi ^{1}} \not = \emptyset$ iff

• 1. $\varPhi ^{1}(x) \in D_{\varPhi ^{1}}$ for a variable x,

• 2. $\varPhi ^{1}(C_v ) = v$,

• 3. $\varPhi ^{1}$ is calculated for terms and other atoms according to $\varOmega _{\varPhi ^{1}}$.

• 4. $\varPhi ^{1}(A \vee B) = \varPhi ^{1}(A) \cup \varPhi ^{1}(B)$,

• 5. $\varPhi ^{1}(A \wedge B) = \varPhi ^{1}(A) \cap \varPhi ^{1}(B)$,

• 6. $\varPhi ^{1}(A \supset B) = \varPhi ^{1}(A) \rightarrow \varPhi ^{1}(B)$,

• 7. $\varPhi ^{1}(\exists x A(x)) = \mathrm{sup}(\varPhi ^{1}(A(d) \, | \, d \in D_{\varPhi ^{1}})$,

• 8. $\varPhi ^{1}(\forall x A(x)) = \mathrm{inf}(\varPhi ^{1}(A(d)) \, | \, d \in D_{\varPhi ^{1}})$.

$$\begin{aligned} \models ^1 A \text{ iff } \forall \varPhi ^{1}: \varPhi ^{1}(A) = 1 \quad \text{ L }^1(L,V, \rightarrow ) = \{A \, | \, \models ^1 A \} \end{aligned}$$

We write $A_1 \ldots A_n \models B$ iff for all $\varPhi ^1$ $\varPhi ^1 (A_1 ) = 1 \text{ and } \ldots \text{ and } \varPhi ^1 (A_n ) = 1$ implies $\varPhi ^1 (B) = 1$.

1 is the only value denoting truth, this justifies the chosen definitions. We omit the superscript in $\models ^0$, $\models ^1$ if the statement holds both for propositional and first-order logic. Quantifier-free first-order formulas can be identified with propositional formulas by identifying different atoms with different variables.

Proposition 1

For all logics the following hold

• i. $\models A \supset A$,

• ii. If $\models B$ then $\models A \supset B$,

• iii. If $\models A \supset B$ and $\models C \supset D$ then $\models (B \supset C) \supset (A \supset D)$.

Example 1

$L = \langle \{0,1,a\}, \le , \cup , \cap , 0, 1 \rangle$, $0< a < 1$

$$\begin{aligned} u \rightarrow v = {\left\{ \begin{array}{ll} 1 \quad u \le v \\ 0 \quad u = 1 \text{ and } v = 0 \\ a \quad \text{ else } \end{array}\right. } \end{aligned}$$

$\mathbf L ^0 (L, \{0,1\}, \rightarrow )$ does not interpolate as

$$\begin{aligned} \models ^0 (x \wedge (x \supset \bot )) \supset (y \vee (y \supset \bot )) \end{aligned}$$

does not interpolate, as the only possible interpolant is a constant with value a, as there are no common variables in the antecedent and the succedent.

$\mathbf L ^0 (L, \{0,a\}, \rightarrow )$ interpolates as all truth constants are representable, $\top$ by $\bot \supset \bot$ (c.f. Sect. 5).

Example 2

Finite propositional and constant-domain Kripke frames can be understood as lattice-based finitely valued logics: Consider upwards closed subsets $\varGamma \subseteq W$, W is the set of worlds, and order them by inclusion. A formula A is assigned the truth value $\varGamma$ iff A is true at exactly the worlds in $\varGamma$.

The constant-domain intuitionistic Kripke frame $\mathcal {K}$ in Fig. 1 is represented by the lattice L in Fig. 2.

Fig. 1.

Constant-domain intuitionistic Kripke frame $\mathcal {K}$.

Fig. 2.

Lattice L.

The propositional language is given by

$$\begin{aligned} \mathcal {L}^{0}\left( L, \left\{ \left( \begin{array}{c} 0 \quad 0 \\ 0 \end{array} \right) \right\} \right) \end{aligned}$$

and the first-order language is given by

$$\begin{aligned} \mathcal {L}^{1}\left( L, \left\{ \left( \begin{array}{c} 0 \quad 0 \\ 0\end{array} \right) \right\} \right) . \end{aligned}$$

The admissible implication of $\mathcal {K}$ is

$$\begin{aligned} u \rightarrow v = {\left\{ \begin{array}{ll} 1 \quad u \le v \\ v \quad \text{ else } \end{array}\right. } \end{aligned}$$

$\le$ determines the lattice.

$$\begin{aligned} \mathrm{MC}= \mathbf L ^0 \left( L, \left\{ \left( \begin{array}{c} 0 \quad 0 \\ 0 \end{array} \right) \right\} , \rightarrow \right) \end{aligned}$$

is the set of valid propositional sentences and

$$\begin{aligned} \mathrm{MC}^\mathrm{QF}= \mathbf L ^1 \left( L, \left\{ \left( \begin{array}{c} 0 \quad 0 \\ 0 \end{array} \right) \right\} , \rightarrow \right) \end{aligned}$$

the set of valid first-order sentences.

Propositional interpolation is easily demonstrated for MC, one of the seven intermediate logics which admit propositional interpolation [13]. Previous proofs for the interpolation of $\mathrm{MC}^\mathrm{QF}$ are quite involved, [17]. In fact, in Sect. 5, Example 5 we will show that this interpolation result is a corollary of the main theorem of this paper.

Definition 6

The occurrence of a formula $\circ$ in a context $C(\circ )$ is inductively defined as

• $C(\circ )$ is $\circ$: the occurrence of $\circ$ is positive,

• $C(\circ )$ is $E(\circ ) \Box F$, $F \Box E(\circ )$, $F \supset E(\circ )$, $Qx E(\circ )$, where $\Box \in \{\wedge , \vee \}$, $Q \in \{\exists , \forall \}$, E, F are formulas: the occurrence of $\circ$ is positive iff the occurrence of $\circ$ in $E(\circ )$ is positive, negative iff the occurrence of $\circ$ in $E(\circ )$ is negative,

• $C(\circ )$ is $E(\circ ) \supset F$, where E, F are formulas: the occurrence of $\circ$ is positive iff the occurrence of $\circ$ in $E(\circ )$ is negative, negative iff the occurrence of $\circ$ in $E(\circ )$ is positive.

Definition 7

If a $\forall$ quantifier or an $\exists$ quantifier occurs positively or negatively, respectively, it is referred to as a strong quantifier. If a $\forall$ quantifier or an $\exists$ quantifier occurs negatively or positively, respectively, it is referred to as a weak quantifier.

Due to the general definition of $\rightarrow$ we have to prove the following Lemma.

Lemma 1

For formulas A, B and a corresponding context $C( \circ )$ it holds

$$\begin{aligned} \text{ if } \quad \models A \supset B \quad \text{ then } \quad \models C(A) \supset C(B) \end{aligned}$$

if $\circ$ occurs positively and

$$\begin{aligned} \text{ if } \quad \models A \supset B \quad \text{ then } \quad \models C(B) \supset C(A) \end{aligned}$$

if $\circ$ occurs negatively.

Proof

We proof the lemma by induction on the structure of the context $C( \circ )$.

• 1. If $C(\circ )$ is $\circ$ or $C_v$, the claim holds trivially.

• 2. If $C(\circ )$ is $E(\circ ) \wedge F$ and $\circ$ occurs positively in $E(\circ )$, then $\circ$ occurs positively in $E(\circ ) \wedge F$.

  $$\begin{aligned} \text{ If } \quad \models A \supset B \quad \text{ then } \quad \models C(A) \supset C(B) \end{aligned}$$

  as by induction hypothesis

  $$\begin{aligned} \text{ if } \quad \models A \supset B \quad \text{ then } \quad \models E(A) \supset E(B) \end{aligned}$$

  and

  $$\begin{aligned} \text{ if } \quad \models E(A) \supset E(B) \quad \text{ then } \quad \models E(A) \wedge F \supset E(B) \wedge F. \end{aligned}$$

  If $C(\circ )$ is $E(\circ ) \wedge F$ and $\circ$ occurs negatively in $E(\circ )$, then $\circ$ occurs negatively in $E(\circ ) \wedge F$.

  $$\begin{aligned} \text{ If } \quad \models A \supset B \quad \text{ then } \quad \models C(B) \supset C(A) \end{aligned}$$

  as by induction hypothesis

  $$\begin{aligned} \text{ if } \quad \models A \supset B \quad \text{ then } \quad \models E(B) \supset E(A) \end{aligned}$$

  and

  $$\begin{aligned} \text{ if } \quad \models E(B) \supset E(A) \quad \text{ then } \quad \models E(B) \wedge F \supset E(A) \wedge F. \end{aligned}$$

  Analogously if $C(\circ )$ is $E \wedge F(\circ )$.

• 3. If $C(\circ )$ is $E(\circ ) \vee F$ and $\circ$ occurs positively in $E(\circ )$, or $\circ$ occurs negatively in $E(\circ )$, similar to 2, analogously if $C(\circ )$ is $E \vee F(\circ )$.

• 4. If $C(\circ )$ is $E(\circ ) \supset F$ and $\circ$ occurs positively in $E(\circ )$ then $\circ$ occurs negatively in $E(\circ ) \supset F$.

  $$\begin{aligned} \text{ If } \quad \models A \supset B \quad \text{ then } \quad \models C(B) \supset C(A) \end{aligned}$$

  as by induction hypothesis

  $$\begin{aligned} \text{ if } \quad \models A \supset B \quad \text{ then } \quad \models E(A) \supset E(B). \end{aligned}$$

  The claim follows by Proposition 1. If $C(\circ )$ is $E(\circ ) \supset F$ and $\circ$ occurs negatively in $E(\circ )$ then $\circ$ occurs positively in $E(\circ ) \supset F$.

  $$\begin{aligned} \text{ If } \quad \models A \supset B \quad \text{ then } \quad \models C(A) \supset C(B) \end{aligned}$$

  as by induction hypothesis

  $$\begin{aligned} \text{ if } \quad \models A \supset B \quad \text{ then } \quad \models E(B) \supset E(A). \end{aligned}$$

  The claim follows by Proposition 1. If $C(\circ )$ is $E \supset F(\circ )$ and $\circ$ occurs positively in $F(\circ )$ or $\circ$ occurs negatively in $F(\circ )$ similar to 2.

• 5. If $C(\circ )$ is $\exists x D(\circ )$ and $\circ$ occurs positively in $D(\circ )$ then $\circ$ occurs positively in $\exists x D(\circ )$.

  $$\begin{aligned} \text{ If } \quad \models A \supset B \quad \text{ then } \quad \models C(A) \supset C(B) \end{aligned}$$

  as by induction hypothesis

  $$\begin{aligned} \text{ if } \quad \models A \supset B \quad \text{ then } \quad \models D(A) \supset D(B). \end{aligned}$$

  and

  $$\begin{aligned} \text{ if } \quad \models D(A) \supset D(B) \quad \text{ then } \quad \models \exists x D(A) \supset \exists x D(B). \end{aligned}$$

  Analogously if $C(\circ )$ is $\exists x D(\circ )$ and $\circ$ occurs negatively in $D(\circ )$.

• 6. If $C(\circ )$ is $\forall x D(\circ )$ and $\circ$ occurs positively in $D(\circ )$ then $\circ$ occurs positively in $\forall x D(\circ )$ similar to 5.

3 Skolemization

We use skolemization to replace strong quantifiers in valid formulas such that the original formulas can be recovered. Note that several Skolem functions for the replacement of a single quantifier are necessary to represent proper suprema and proper infima. We fix L $(L,V, \rightarrow )$, $L = \langle W, \le , \cup , \cap , 0, 1 \rangle$.

Definition 8

Consider a formula B in a context A(B). Then its skolemization A(sk(B)) is defined as follows:

Replace all strong quantifier occurrences (positive occurrence of $\forall$ and negative occurrence of $\exists$) (note that no quantifiers in A bind variables in B) of the form $\exists x C(x)$ (or $\forall x C(x)$) in B by $\bigvee _{i = 1}^{|W|} C(f_i (\overline{x}))$ (or $\bigwedge _{i = 1}^{|W|}C(f_i (\overline{x}))$), where $f_i$ are new function symbols and $\overline{x}$ are the weakly quantified variables of the scope.

Skolem axioms are closed sentences

$$\begin{aligned} \forall \overline{x} (\exists y A(y, \overline{x}) \supset \bigvee _{i=1}^{|W|} A(f_{i}(\overline{x}), \overline{x}) \quad \text{ and } \quad \forall \overline{x} (\bigwedge _{i=1}^{|W|} A(f_{i}(\overline{x}), \overline{x}) \supset \forall y A(y, \overline{x})) \end{aligned}$$

where $f_i$ are new function symbols (Skolem functions).

Lemma 2

• 1. If $\models ^1 A(B)$ then $\models ^1 A(sk(B))$.

• 2. If $S_1 \ldots S_k \models ^1 A(sk(B))$ then $S_1 \ldots S_k \models ^1 A(B )$, for suitable Skolem axioms $S_1 \ldots S_k$.

• 3. If $S_1 \ldots S_k \models ^1 A$, where $S_1 \ldots S_k$ are Skolem axioms and A does not contain Skolem functions then $\models ^1 A$.

Proof

• 1. Note that

  $$\begin{aligned} \text{ if } \quad \models A(D) \quad \text{ then } \quad \models A(D \vee D) \end{aligned}$$

  and

  $$\begin{aligned} \text{ if } \quad \models A(D) \quad \text{ then } \quad \models A(D \wedge D). \end{aligned}$$

  Use Lemma 1 and

  $$\begin{aligned} \models ^1 D'(t) \supset \exists x D'(x), \quad \models ^1 \forall x D'(x) \supset D'(t). \end{aligned}$$

• 2. Use Lemma 1 and suitable Skolem axioms to reconstruct strong quantifiers.

• 3. Assume . As usual, we have to extend the valuation to the Skolem functions to verify the Skolem axioms. There is a valuation in $\langle D_{\varPhi ^1}, \varOmega _{\varPhi ^1} \rangle$ s.t. $\varPhi ^{1}(A) \not = 1$. Using at most |W| Skolem functions and AC we can always pick witnesses as values for the Skolem functions such that the first-order suprema and infima are reconstructed on the propositional level. (AC is applied to sets of objects where the corresponding truth value is taken.)

  $$\begin{aligned} \mathrm{sup}\{\varPhi ^{1}(B(f_i (\overline{t}), \overline{t})) \, | \, 1 \le i \le |W| \} = \end{aligned}$$
  $$\begin{aligned} \mathrm{sup}\{\varPhi ^{1}(B(d, \overline{t}) \, | \, d \in D_{\varPhi ^{1}} \} = \varPhi ^{1}(\exists y B(y, \overline{t})) \end{aligned}$$

  and

  $$\begin{aligned} \mathrm{inf}\{\varPhi ^{1}(B(f_i (\overline{t}), \overline{t})) \, | \, 1 \le i \le |W|\} = \end{aligned}$$
  $$\begin{aligned} \mathrm{inf}\{\varPhi ^{1}(B(d, \overline{t})) \, | \, d \in D_{\varPhi ^{1}} \} = \varPhi ^{1}(\forall y B(y, \overline{t})). \end{aligned}$$

Example 3

We continue with the logic $\mathrm{MC}^\mathrm{QF}$ introduced in Example 2. For the given logic

$$\begin{aligned} \exists x B(x) \supset sk(\exists y \forall z C(y,z)) \equiv \exists x B(x) \supset \exists y \bigwedge _{i = 1}^{5} C(y, f_i(y)). \end{aligned}$$

4 Expansions

Expansions, first introduced in [15], are natural structures representing the instantiated variables for quantified formulas. They record the substitutions for quantifiers in an effort to recover a sound proof of the original formulation of Herbrand’s Theorem. As we work with skolemized formulas, in this paper we we consider only expansions for formulas with weak quantifiers. Consequently the arguments are simplified.

In the following we assume that a constant c is present in the language and that $t_1 , t_2, \ldots$ is a fixed ordering of all closed terms (terms not containing variables).

Definition 9

A term structure is a structure $\langle D, \varOmega \rangle$ such that D is the set of all closed terms.

Proposition 2

Let $\varPhi ^1 (\exists x A(x)) = \upsilon$ in a term structure. Then $\varPhi ^1 (\exists x A(x) = \varPhi ^1 (\bigvee _{i = 1}^{n} A(t_i ))$ for some n. Analogously for $\forall x A(x)$, i.e. let $\varPhi ^1 (\forall x A(x)) = \upsilon$ in a term structure, then $\varPhi ^1 (\forall x A(x)) = \varPhi ^1 (\bigwedge _{i=1}^{n} A(t_i ))$ for some n.

Proof

Only finitely many truth values exists, therefore there is an n such that the valuation becomes stable on $\bigvee _{i=1}^n A(t_i )$ ($\bigwedge _{i=1}^n A(t_i )$).

Definition 10

Let E be a formula with weak quantifiers only. The n-th expansion $E_n$ of E is obtained from E by replacing inside out all subformulas $\exists x A(x)$ ($\forall x A(x)$) by $\bigvee _{i=1}^n A(t_i )$ ($\bigwedge _{i=1}^n A(t_i )$). $E_n$ is a Herbrand expansion iff $E_n$ is valid. In case there are only m terms $E_{m+k} = E_m$.

Lemma 3

Let $\varPhi ^1 (E) = \upsilon$ in a term structure. Then there is an n such that for all $m \ge n$ $\varPhi ^1 (E_m ) = \upsilon$.

Proof

We apply Proposition 2 outside in to replace subformulas $\exists x$ A(x) ($\forall x$ A(x)) stepwise by $\bigvee _{i=1}^n$ $A(t_i )$ ($\bigwedge _{i=1}^n$ $A(t_i )$) without changing the truth value. The disjunctions and conjunctions can be extended to common maximal disjunctions and conjunctions.

Theorem 1

Let E contain only weak quantifiers. Then $\models E$ iff there is a Herbrand expansion $E_n$ of E.

Proof

$\Rightarrow$: Assume $\models E$ but for all n. Let $\varGamma _i = \{\varPhi _{i,v}^0 | \varPhi _{i,v}^0 (E_i) \not = 1\}$ and define $\varGamma = \bigcup \varGamma _i$. Note that the first index in $\varPhi ^0_{i,v}$ relates to the expansion level and the second index to all counter-valuations at this level. Assign a partial order < to $\varGamma$ by $\varPhi _{i,v}^0 < \varPhi _{j,w}^0$ for $\varPhi _{i,v}^0 \in \varGamma _i$, $\varPhi _{j,w}^0 \in \varGamma _j$ and $i < j$ iff $\varPhi _{i,v}^0$ and $\varPhi _{j,w}^0$ coincide on the atoms of $E_i$. By König’s Lemma there is an infinite branch $\varPhi _{1,i_{1}}^0< \varPhi _{2, i_{2}}^0 < \ldots$. Define a term structure induced by an evaluation on atoms P:

$$\begin{aligned} \varPhi ^1 (P) = {\left\{ \begin{array}{ll} \upsilon \quad P \text{ occurs } \text{ in } \text{ some } E_n \text{ and } \varPhi _{n, i_{n}} (P) = \upsilon \\ 1 \quad \text{ else } \end{array}\right. } \end{aligned}$$

$\varPhi ^1 (E) \not = 1$ by Lemma 3.

$\Leftarrow$: Use Lemma 1 and $\models A(t) \supset \exists x A(x)$ and $\models \forall x A(x) \supset A(t)$. Note that

$$\begin{aligned} \text{ if } \quad \models A(D \vee D) \quad \text{ then } \quad \models A(D) \end{aligned}$$

and

$$\begin{aligned} \text{ if } \quad \models A(D \wedge D) \quad \text{ then } \quad \models A(D). \end{aligned}$$

Example 4

Consider the lattice in Example 2, Fig. 2 and the term ordering $c < d$. The expansion sequence of $P(c,d,d) \supset \exists x P(c,x,d)$ is

$$\begin{aligned} E_1 = P(c,d,d) \supset P(c,c,d), E_2 = P(c,d,d) \supset P(c,c,d) \vee P(c,d,d), E_{2+k} = E_2 . \end{aligned}$$

The second formula is a Herbrand expansion.

5 The Interpolation Theorem

Theorem 2

Interpolation holds for $\mathbf{L }^{0}(L,V,\rightarrow )$ iff interpolation holds for $\mathbf{L }^{1}(L,V,\rightarrow )$.

Proof

$\Leftarrow$: trivial.

$\Rightarrow$: Assume $A \supset B \in \mathcal {L}(L,V)$ and $\models A \supset B$.

$$\begin{aligned} \models sk(A) \supset sk(B) \quad \text{ by } \text{ Lemma } \text{2 } \text{1. } \end{aligned}$$

Construct a Herbrand expansion $A_H \supset B_H$ of $sk(A) \supset sk(B)$ by Theorem 1. Construct the propositional interpolant $I^*$ of $A_H \supset B_H$,

$$\begin{aligned} \models A_H \supset I^* \quad \text{ and } \quad \models I^* \supset B_H . \end{aligned}$$

Use Lemma 1 and

$$\begin{aligned} \models A(t) \supset \exists x A(x), \quad \models \forall x A(x) \supset A(t) \end{aligned}$$

to obtain

$$\begin{aligned} \models sk(A) \supset I^* \quad \text{ and } \quad \models I^* \supset sk(B) \end{aligned}$$

Order all terms f(t) in $I^*$ by inclusion where f is not in the common language. Let $f^{*}(\overline{t})$ be the maximal term.

• i. $f^*$ is not in sk(A). Replace $f^{*}(\overline{t})$ by a fresh variable x to obtain

  $$\begin{aligned} \models sk(A) \supset I^{*} \{x / f^{*}(\overline{t})\}. \end{aligned}$$

  But then also

  $$\begin{aligned} \models sk(A) \supset \forall x I^{*} \{x / f^{*}(\overline{t})\} \end{aligned}$$

  and

  $$\begin{aligned} \models \forall x I^{*} \{x / f^{*}(\overline{t})\} \supset sk(B) \end{aligned}$$

  by

  $$\begin{aligned} \models \forall x I^{*} \{x / f^{*}(\overline{t})\} \supset I^{*}. \end{aligned}$$

• ii. $f^*$ is not in sk(B). Replace $f^{*}(\overline{t})$ by a fresh variable x to obtain

  $$\begin{aligned} \models I^{*} \{x / f^{*}(\overline{t})\} \supset sk(B). \end{aligned}$$

  But then also

  $$\begin{aligned} \models \exists x I^{*} \{x / f^{*}(\overline{t})\} \supset sk(B) \end{aligned}$$

  and

  $$\begin{aligned} \models sk(A) \supset \exists x I^{*} \{x / f^{*}(\overline{t})\} \end{aligned}$$

  by

  $$\begin{aligned} \models I^* \supset \exists x I^{*} \{x \backslash f^{*}(\overline{t})\}. \end{aligned}$$

Repeat this procedure till all functions and constants not in the common language (among them the Skolem functions) are eliminated from the middle formula. Let I be the result. I is an interpolant of $sk(A) \supset sk(B)$. By Lemma 2 2,3 I is an interpolant of $A \supset B$. For a similar construction for classical first-order logic see Chap. 8.2 of [4].

Corollary 1

If interpolation holds for L $^{0}(L,V,\rightarrow )$, $\quad \models A \supset B$ and $A \supset B$ contains only weak quantifiers, then there is a quantifier-free interpolant with common predicates for $A \supset B$.

Remark 1

Corollary 1 cannot be strengthened to provide a quantifier-free interpolant with common predicate symbols and common function symbols for $A \supset B$. Consider

$$\begin{aligned} Q_\forall A(x_1 , f_1(x_1), x_2 , f_2 (x_1 , x_2) , \ldots ) \supset Q_\exists A(g_1 , y_1 , g_2 (y_1), y_2 , g_3 (y_1 , y_2), \ldots ), \end{aligned}$$

where $Q_\forall = \forall x_1 \forall x_2 \ldots$ and $Q_\exists = \exists y_1 \exists y_2 \ldots$. This is the skolemization of

$$\begin{aligned} \forall x_1 \exists x'_1 \forall x_2 \ldots A(x_1 , x'_1, x_2 , \ldots ) \supset \forall x_1 \exists x'_1 \forall x_2 \ldots A(x_1 , x'_1, x_2 , \ldots ), \end{aligned}$$

where $\forall x_1 \exists x'_1 \forall x_2 \exists x'_2 \ldots A(x_1 , x'_1, x_2 , x'_2, \ldots )$ is the only possible interpolant modulo provable equivalence with common predicate and function symbols.

Example 5

Example 2 continued. For the given logic we calculate the interpolant for

$$\begin{aligned} \exists x (B(x) \wedge \forall y C(y)) \supset \exists x (A(x) \vee B(x)). \end{aligned}$$

• 1. Skolemization

  $$\begin{aligned} \bigvee _{i=1}^{5}(B(c_i) \wedge \forall y C(y)) \supset \exists x (A(x) \vee B(x)). \end{aligned}$$

• 2. Herbrand expansion

  $$\begin{aligned} \bigvee _{i=1}^{5}(B(c_i) \wedge C(c_1 )) \supset \bigvee _{i=1}^{5} (A(c_i ) \vee B(c_i )). \end{aligned}$$

• 3. Propositional interpolant

  $$\begin{aligned} \bigvee _{i=1}^{5}(B(c_i) \wedge C(c_1 )) \supset \bigvee _{i=1}^{5}B(c_i ) \quad \bigvee _{i=1}^{5}B(c_i ) \supset \bigvee _{i=1}^{5}(A(c_i ) \vee B(c_i )). \end{aligned}$$

• 4. Back to the Skolem form

  $$\begin{aligned} \bigvee _{i=1}^{5}(B(c_i) \wedge \forall y C(y)) \supset \bigvee _{i=1}^{5}B(c_i ) \quad \bigvee _{i=1}^{5}B(c_i ) \supset \exists x (A(x) \vee B(x)). \end{aligned}$$

• 5. Elimination of function symbols and constants not in the common language from $\bigvee _{i=1}^{5}B(c_i )$. Result:

  $$\begin{aligned} \exists z_1 \ldots \exists z_5 \bigvee B(z_i ). \end{aligned}$$

• 6. Use the Skolem axiom

  $$\begin{aligned} \exists x (B(x) \wedge \forall y C(y)) \supset \bigvee _{i=1}^{5} B(c_i ) \wedge \forall y C(y) \end{aligned}$$

  to reconstruct the original first-order form.

• 7. The Skolem axiom can be deleted.

Proposition 3

Let $L = \langle W, \le , \cup , \cap , 0, 1 \rangle$.

• i. L $^0 (L, \emptyset , \rightarrow )$ (and therefore L $^1 (L, \emptyset , \rightarrow )$) never has the interpolation property.

• ii. L $^0 (L, W, \rightarrow )$ (and therefore L $^1 (L, W, \rightarrow )$) always has the interpolation property.

Proof

• i. $\models ^0 x \supset (y \supset y)$ and the only possible interpolant is $\top$, which is not variable-free definable.

• ii. Consider $\models A(x_1 , \ldots ,x_n , y_1 , \ldots , y_m) \supset B(y_1 \ldots y_n , z_1 , \ldots z_o),$

  $$\begin{aligned} I = \bigvee _{\langle v_{i_1}, \ldots v_{i_n} \rangle \in W \times W} A(C_{v_{i_1}}, \ldots , C_{v_{i_n}}, y_1 , \ldots , y_m) \end{aligned}$$

  is an interpolant as

  $$\begin{aligned} \models A(x_1 , \ldots ,x_n , y_1 , \ldots , y_m) \supset I \end{aligned}$$

  and

  $$\begin{aligned} \models I \supset B(y_1 \ldots y_n , z_1 , \ldots z_o) \end{aligned}$$

  by substitution.

Proposition 3 ii. makes it possible to characterize all extensions of a lattice based many-valued logic which admit first-order interpolation.

$$\begin{aligned} \text{ SPECTRUM }(L, \rightarrow ) = \{V \, | \, \mathbf L ^1 (L, V, \rightarrow ) \text { interpolates}\}. \end{aligned}$$

Example 6

$L = \langle \{0,1\}, \le , \cup , \cap , 0, 1 \rangle$ the lattice of classical logic, $\rightarrow$ classical implication.

$$\begin{aligned} \text{ SPECTRUM }(L, \rightarrow ) = \{\{0\}, \{1\}, \{0,1\}\} \end{aligned}$$

This is the maximal possible spectrum by Proposition 3 i.

L $^0 (L, \{0\}, \rightarrow )$ and L $^0 (L, \{0, 1\}, \rightarrow )$ interpolate as all truth constants are representable by closed formulas, therefore L $^1 (L, \{0\}, \rightarrow )$ and L $^1 (L, \{0, 1\}, \rightarrow )$ interpolate (Craig’s result, which does however not cover L $^1 (L, \{1\}, \rightarrow )$).

To show that L $^0 (L, \{1\}, \rightarrow )$ interpolates first note that in general

$$\begin{aligned} \bigvee _i E_i \supset \bigwedge _j F_j \end{aligned}$$

interpolates iff there are interpolants

$$\begin{aligned} E_i \supset I_{ij} \quad I_{ij} \supset F_j. \end{aligned}$$

$\bigwedge _j \bigvee _i I_{ij}$ is a suitable interpolant. Now use the value presenting transformations

$$\begin{aligned} D(A \wedge B \supset C) \quad \Rightarrow \quad D(A \supset C \vee B \supset C) \end{aligned}$$

$$\begin{aligned} D(A \vee B \supset C) \quad \Rightarrow \quad D(A \supset C \wedge B \supset C) \end{aligned}$$

$$\begin{aligned} D((A \supset B) \supset C) \quad \Rightarrow \quad D(C \vee (A \wedge (B \supset C))) \end{aligned}$$

$$\begin{aligned} D(x) \quad \Rightarrow \quad D(\top \supset x) \end{aligned}$$

for variables x together with distributions and simplifications, to reduce the problem to

$$\begin{aligned} \bigwedge _i (u_i \supset v_i ) \supset \bigvee _j (s_j \supset t_j ) \end{aligned}$$

$v_i , t_j$ variables, $u_i , s_j$ variables or $\top$. We assume that the succedent is not valid (otherwise $\top$ is the interpolant). So any variable occurs either in the $s_j$ group or in the $t_j$ group. Close the antecedents under transitivity of $\supset$. There is a common implication $u \supset v$, an interpolant (Otherwise there is a countervaluation by assigning 0 to all $t_j$ and extending this assignment in the antecedent such that if $v_i$ is assigned 0 also $u_i$ is assigned 0. No $s_j$ is assigned 0 by this procedure. Assign 1 to all other variables and derive a contradiction to the assumption, that the initial implication is valid). Therefore, L $^1 (L, \{1\}, \rightarrow )$ interpolates.

Example 7

n-valued Gödel logics.

Let $G_n = \langle W_n , \le , \cup , \cap , 0, 1 \rangle$, where $W_n = \{ 0, \frac{1}{n-1}, \ldots , \frac{n-2}{n-1}, 1 \}$, $\le$ is the natural order and $\cup , \cap , 0, 1$ are defined accordingly.

$$\begin{aligned} u \rightarrow v = {\left\{ \begin{array}{ll} 1 \quad u \le v \\ v \quad \text{ else } \end{array}\right. } \end{aligned}$$

The first-order spectrum in the presence of $\bot$ consists of all sets of truth values $\{\bot \} \cup (\varGamma - \{\bot , \top \})$ and $\{\bot ,\top \} \cup (\varGamma - \{\bot ,\top \})$ such that there are no consecutive truth values $\upsilon _i , \upsilon _{i+1}$ both not in $\varGamma - \{\bot ,\top \}$ (see [6]).

6 Extensions to Infinitely-Valued Logics

We may use the described methodology to prove interpolation for (fragments of) infinitely-valued logics, as for instance Gödel logics [5]. Consider Gödel logic $\mathrm{G}_{[0,1]}^\mathrm{QF}$, the logic of all linearly ordered Kripke frames with constant domains. Its connectives can be interpreted as functions over the real interval [0, 1] as follows: $\bot$ is the logical constant for 0, $\vee , \wedge , \exists , \forall$ are defined as maximum, minimum, supremum, infimum, respectively. $\lnot A$ is an abbreviation for $A \rightarrow \bot$ and $\rightarrow$ is defined as

$$\begin{aligned} u \rightarrow v = {\left\{ \begin{array}{ll} 1 \quad u \le v \\ v \quad \text{ else } \end{array}\right. } \end{aligned}$$

The weak quantifier fragment of $\mathrm{G}_{[0,1]}^\mathrm{QF}$ admits Herbrand expansions. This follows from cut-free proofs in hypersequent calculi [2]. This can be easily shown by proof transformation steps in the hypersequent calculus. Indeed, we can transform proofs by eliminating weak quantifier inferences:

• i. If there is an occurrence of an $\exists$ introduction, we select all formulas $A_i$ that correspond to this inference and eliminate the $\exists$ introduction by the use of $\bigvee _i A_i$.

• ii. If there is an occurrence of a $\forall$ introduction, we select all formulas $B_i$ that correspond to this inference and eliminate the $\forall$ introduction by the use of $\bigwedge _i B_i$.

We suppress the inference of weak quantifiers and combine the disjunctions respectively conjunctions to accommodate contractions. Propositional Gödel logic interpolates and therefore the weak quantifier fragment of $G^{QF}_{[0,1]}$ interpolates too, as no skolemization is necessary.

The fragment $A \supset B$, A, B prenex also interpolates: Skolemize as in classical logic, construct a Herbrand expansion, interpolate, go back to the Skolem form and use an immediate analogy of the 2nd $\varepsilon$-theorem [11] to go back to the original formulas. To illustrate the procedure, consider the following example.

Example 8

$$\begin{aligned} \mathrm{G}_{[0,1]}^\mathrm{QF}\models \forall x \exists y (P(x) \wedge Q(y)) \supset \forall x \exists y (R(x) \vee P(y)) \end{aligned}$$

We skolemize as in classical logic (note that the substitution of Skolem terms is always possible).

$$\begin{aligned} \mathrm{G}_{[0,1]}^\mathrm{QF}\models \forall x (P(x) \wedge Q(f(x))) \supset \exists y (R(c) \vee P(y)). \end{aligned}$$

Calculate a Herbrand expansion

$$\begin{aligned} \mathrm{G}_{[0,1]}^\mathrm{QF}\models P(c) \wedge Q(f(c)) \supset R(c) \vee P(c). \end{aligned}$$

Construct a propositional interpolant

$$\begin{aligned} \mathrm{G}_{[0,1]}^\mathrm{QF}\models P(c) \wedge Q(f(c)) \supset P(c) \quad \mathrm{G}_{[0,1]}^\mathrm{QF}\models P(c) \supset R(c) \vee P(c). \end{aligned}$$

Go back to the Skolem form

$$\begin{aligned} \mathrm{G}_{[0,1]}^\mathrm{QF}\models \forall x (P(x) \wedge Q(f(x))) \supset P(c) \quad \mathrm{G}_{[0,1]}^\mathrm{QF}\models P(c) \supset \exists x (R(c) \vee P(x)). \end{aligned}$$

Eliminate c from the interpolant

$$\begin{aligned} \mathrm{G}_{[0,1]}^\mathrm{QF}\models \forall x (P(x) \wedge Q(f(x))) \supset \forall x P(x) \quad \mathrm{G}_{[0,1]}^\mathrm{QF}\models \forall x P(x) \supset \exists x (R(c) \vee P(x)). \end{aligned}$$

Skolemize the interpolant in both formulas and construct a Herbrand expansion to apply the 2nd $\varepsilon$-Theorem to obtain

$$\begin{aligned} \mathrm{G}_{[0,1]}^\mathrm{QF}\models \forall x \exists y (P(x) \wedge Q(y)) \supset \forall x P(x) \quad \mathrm{G}_{[0,1]}^\mathrm{QF}\models \forall x P(x) \supset \forall x \exists y (R(x) \vee P(y)). \end{aligned}$$

• i. $\mathrm{G}_{[0,1]}^\mathrm{QF}\models P(e) \wedge Q(f(e)) \supset P(e)$: replace all Skolem terms by variables representing them.

  $$\begin{aligned} \mathrm{G}_{[0,1]}^\mathrm{QF}\models P(x_e ) \wedge Q(x_e ) \supset P(x_e ). \end{aligned}$$

  Infer weak quantifiers, shift and contract as much as possible, otherwise infer the strong quantifier representing a deepest Skolem term available, shift and repeat.

  $$\begin{aligned} \mathrm{G}_{[0,1]}^\mathrm{QF}\models \exists y (P(x_e ) \wedge Q(y)) \supset P(x_e ) \end{aligned}$$
  $$\begin{aligned} \mathrm{G}_{[0,1]}^\mathrm{QF}\models \forall x \exists y (P(x) \wedge Q(y)) \supset P(x_e ) \end{aligned}$$
  $$\begin{aligned} \mathrm{G}_{[0,1]}^\mathrm{QF}\models \forall x \exists y (P(x) \wedge Q(y)) \supset \forall x P(x) \end{aligned}$$

• ii. $\mathrm{G}_{[0,1]}^\mathrm{QF}\models P(c) \supset R(c) \vee P(c)$:

  $$\begin{aligned} \mathrm{G}_{[0,1]}^\mathrm{QF}\models P(x_c ) \supset R(x_c ) \vee P(x_c ) \end{aligned}$$
  $$\begin{aligned} \mathrm{G}_{[0,1]}^\mathrm{QF}\models \forall x P(x) \supset R(x_c ) \vee P(x_c ) \end{aligned}$$
  $$\begin{aligned} \mathrm{G}_{[0,1]}^\mathrm{QF}\models \forall x P(x) \supset \exists y (R(x_c ) \vee P(y)) \end{aligned}$$
  $$\begin{aligned} \mathrm{G}_{[0,1]}^\mathrm{QF}\models \forall x P(x) \supset \forall x \exists y (R(x) \vee P(y)) \end{aligned}$$

Therefore, it is possible to show interpolation for fragments of $\mathrm{G}_{[0,1]}^\mathrm{QF}$, however, not yet for $\mathrm{G}_{[0,1]}^\mathrm{QF}$. What lacks to prove interpolation for $\mathrm{G}_{[0,1]}^\mathrm{QF}$ is a suitable skolemization of all formulas!

7 Conclusion

Extending the notion of expansion to formulas containing strong quantifiers might be possible to cover logics which do not admit skolemization, e.g. logics based on non-constant domain Kripke frames (such notions of expansion are in the spirit of Herbrand’s original proof of Herbrand’s Theorem).

Another possibility is to develop unusual skolemizations e.g. based on existence assumptions [3] or on added Skolem predicates instead of Skolem functions as in [10].

The methodology of this paper can also be used to obtain negative results. First-order S5 does not interpolate by a well-known result of Fine [9]. As propositional S5 interpolates, first-order S5 cannot admit skolemization together with expansions in general.