Interpolation Theorems for Intuitionistic Predicate Logic

G. Mints

April 1998

Abstract

Craig interpolation theorem (which holds for intuitionistic logic) implies that the derivability of X,X’-¿Y’ implies existence of an interpolant I in the common language of X and X’-¿Y’ such that both X-¿I and I,X’-¿Y’ are derivable. For classical logic this extends to X,X’-¿Y,Y’, but for intuitionistic logic there are counterexamples. There is a version true for intuitionistic propositional (but not for predicate) logic, and more complicated version for the predicate case.

Contents

1 Introduction 2

2 A Symmetric Interpolation Theorem 2

3 An Interpolation Theorem for Multiple Succedent Sequents 7

4 Kripke-style System 9 4.1 System KInt . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 4.2 Analytic Cut . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

1 Introduction

Craig interpolation theorem (which holds for intuitionistic logic) implies that the derivability of Γ, Γ′ ⇒ Δ′ implies existence of a Craig interpolant I in the common language of Γ and Γ′ ⇒ Δ′ such that both Γ ⇒ I and I, Γ′ ⇒ Δ′ are derivable. For classical logic this extends to the partition Γ; Γ′ ⇒ Δ; Δ′, i.e. there is an interpolant I satisfying Γ ⇒ Δ, I and I, Γ′ ⇒ Δ′. For intuitionistic logic there are counterexamples. Indeed for the partition ; C ⇒ C; the interpolant I should satisfy ⇒ C, I and I, C ⇒. By the disjunction property one of C, I should be derivable: a contradiction.

Nevertheless some interpolation properties for disjunction are true also in the intuitionistic case. We present here is a multi-succedent version of interpolation true for intuitionistic propositional (but not for predicate) logic, and more complicated version for the predicate case. Kripke-style formulation in terms of sequents indexed by possible worlds is considered in the last section. A result similar to symmetric interpolation was established by L. Maksimova in [11].

One of the motivations for the present work comes from the study of interpolation in the (superintuitionistic) logic of constant domains.

L_{E} denotes below the language of the expression (formula, sequent etc.) E. Recall that a sequent A_{1}, …, A_{n} ⇒ B_{1}, …, B_{m} is interpreted as &_{i}A_{i} → ∨_{j}B_{j}. ≡ will denote syntactical identity of expressions. We write Γ ⊢ Δ to indicate that the sequent Γ ⇒ Δ is intuitionistically derivable.

The results of the first three sections were obtained when the author visited the Institute for Logic, Language and Information of the University of Amsterdam in the framework of Spinoza project headed by Johan van Benthem.

2 A Symmetric Interpolation Theorem

Definition 1 Let v_{1}, …, v_{p} be distinct propositional variables and

T_{1}; T_{2}; …; T_{k}  k ≥ 2  (1)

be sequents with distinct antecedent and succedent terms all among v_{1}, …, v_{p}, for example

v_{2}, v_{3} ⇒ v_{1}, v_{4}; ⇒ v_{2}; ⇒ v_{3}; v_{1} ⇒; v_{4} ⇒  (2)

We say that (1) is balanced iff it is classically inconsistent.

Note 1. By the completeness of the resolution rule (1) is balanced iff the empty sequent ⇒ is derivable from (1) by a series of cuts

cut \frac{Γ ⇒ Δ, A A, Σ ⇒ Π}{Γ ∪ Σ ⇒ Δ ∪ Π}

where identical terms in Γ, Σ and Δ, Π are contracted. Note that cut is intuitionistically valid.

Example. (2) is balanced; the empty sequent is obtained by four cuts successively eliminating variables v_{i} in arbitrary order.

Definition 2 If S ≡ Γ ⇒ Δ, S′ ≡ Γ′ ⇒ Δ′ then (following [4]) SS′ ≡ Γ, Γ′ ⇒ Δ, Δ′.

Classically SS′ corresponds to S ∨ S′.

Definition 3 Let S, S′ be arbitrary sequents, I_{1}, …, I_{p} be formulas, v_{1}, …, v_{p} be distinct new propositional variables, and (1) be a list of sequents composed from v_{1}, …, v_{p}. We say that

(I_{1}, …, I_{p}; T_{1}; …; T_{p})  (3)

is an interpolant for S, S′ iff all predicate symbols of I_{1}, …, I_{p} are common to S and S′, the list T_{1}; …; T_{k} is balanced and there is an m (1 ≤ m < k) such that all sequents

ST_{1}^{∗}, …, ST_{m}^{∗}, S′T_{m+1}^{∗}, …, S′T_{k}^{∗}  (4)

are derivable, where T^{∗} = T [v_{1}/I_{1}, …, v_{p}/I_{p}]

Lemma 1 (a) If there is an interpolant for S, S′ then SS′ is derivable.

(b) From an interpolant for E ⇒, ⇒ F one can (easily) construct a Craig interpolant for E → F and vice versa

Proof . (a) Use cuts to resolve all components of T_{i}^{∗} from (4).

(b) Assume that

E ⇒ T_{1}^{∗}, …, E ⇒ T_{m}^{∗}, T_{m+1}^{∗} ⇒ F, …, T_{k}^{∗} ⇒ F  (5)

are derivable, and define

I ≡ T_{1}^{∗}& … &T_{m}^{∗}

where sequents are converted into formulas. The set T_{1}^{∗}, …, T_{m}^{∗} is obviously interderivable with I. In particular,

E ⇒ I  (6)

is derivable. To derive

I ⇒ F  (7)

note that T_{1}, …, T_{k} is balanced, and hence by Note 1 there is a deduction of the empty sequent ⇒ from T_{1}^{∗}, …, T_{k}^{∗} by cut rule . Replacing T_{m+1}^{∗}, …, T_{k}^{∗} in this deduction by T_{m+1}^{∗} ⇒ F, …, T_{k}^{∗} ⇒ F and using derivability of these sequents (cf (5)) one gets a deduction of ⇒ F from T_{1}^{∗}, …, T_{m}^{∗} , i.e. from ⇒ I as required.

The formula I may contain some variables x free in E but not in F, and some variables y free in F but not in E. In this case (6,7) imply that the formula ∃x∀yI (or ∀y∃xI ) is a Craig interpolant for E → F. □

Theorem 1 If SS′ is derivable and does not contain negative ∃-quantifiers, then there is an interpolant for SS′.

Proof . We use induction on a cutfree derivation of SS′ which we write as

Γ; Γ′ ⇒ Δ; Δ′

in the multiple succedent version of the intuitionistic predicate logic. Consider possible cases.

Axiom Γ, C, Γ′ ⇒ Δ, C, Δ′.

If both C’s are in S or both are in S′ or the first C is in S and the second C is in S′, then an interpolant is constructed in the standard way, which formally means that (3) in these three cases takes the form:

(⊥; ⇒ v1; v1 ⇒)  (⊤; ⇒ v1; v1 ⇒)  (C; ⇒ v1; v1 ⇒)  (8)

In the following we usually write down only sequent (4), i.e in our three cases

(S ⇒ ⊥; ⊥ ⇒ S′),  (S ⇒ ⊤; ⊤ ⇒ S′)  (S ⇒ C; C ⇒ S′)

instead of (8).

In the remaining subcase of the axiom case (which was the reason for introduction of the whole machinery of composite interpolants) when the first C is in S′ and the second C is in S, the interpolant (4) is C ⇒ S, S′ ⇒ C), i.e. (3) is (C; v_{1} ⇒; ⇒ v_{1}).

Axiom Γ, ⊥, Γ′ ⇒ Δ, Δ′ is treated in the standard way.

Now consider cases depending of the last rule used in the derivation of SS′. By the IH (induction hypothesis) there are interpolants for each of the premises. Let us write the T -part (T_{1}, …, T_{k}) of an interpolant in the form (T, T′) where T = T_{1}, …, T_{m}, T′ = T_{m+1}, …, T_{k} and m is determined by (4), i.e. T, T′ are the parts of the interpolant related to S, S′.

Rule →⇒ (implication antecedent). By IH there are interpolants

(I; T, T′); (J; U, U′)

for premises of the rule. Renaming variables v_{i} if necessary assume that (T, T′) and (U, U′) have no variables in common.

Case 1. The principal formula (A → B) of the inference belomgs to S.Then the interpolant for the conclusion will be

(I, J; T ∨ U; T′ ∪ U′)

where T ∨ U ≡ {T U : T ∈ T, U ∈ U}. The result is balanced:

&(T ∨ U)&&(T′ ∪ U′) ⇒ (&T&T′) ∨ (&U&U′)

and both disjuncts to the right of ⇒ are contradictory by IH. To check other properties of the interpolant, look at the figure:

\frac{S(⇒ A)S′ S(B ⇒)S′}{S(A → B ⇒)S′} S(⇒ A)T S′T′  S(B ⇒)U S′U′

S(A → B ⇒)(T ∨ U)  S′(T′ ∪ U′)

Case 2. (A → B) ∈ S′). Then the interpolant for the conclusion is

(I, J; T ∪ U; T′ ∨ U′)

Rule ⇒→ (implication succedent). Use the Craig interpolant. If for example (A → B) ∈ S, then

\frac{Γ, A, Γ′ ⇒ B}{Γ, Γ′ ⇒ Δ, A → B, Δ′}  Γ′ ⇒ I ; exists by IH  \frac{I, Γ, A ⇒ B}{I, Γ ⇒ Δ, A → B}

Rule & ⇒. The interpolant is preserved. If for example (A&B) ∈ S, then

\frac{S(A, B ⇒)S′}{S, (A&B ⇒)S′}  \frac{S(A, B ⇒)T}{S, (A&B ⇒)T}  S′T′

Rule ⇒ & is treated exactly like →⇒:

\frac{S(⇒ A)S′ S(⇒ B)S′}{S(⇒ A&B)S′} S(⇒ A)T S′T′  S(⇒ B)U S′U′

S(⇒ A&B)(T ∨ U)  S′(T′ ∪ U′)

Rule ∨ ⇒ is treated symmetrically:

\frac{S(A ⇒)S′ S(B ⇒)S′}{S(A ∨ B ⇒)S′} S(A ⇒)T S′T′  S(B ⇒)U S′U′

S(A ∨ B ⇒)(T ∨ U)  S′(T′ ∪ U′)

Rule ⇒ ∨. Interpolant is just preserved, as in the case of & ⇒.

Rules ∀ ⇒, ⇒ ∃. Like & ⇒:

\frac{S(A[t] ⇒)S′}{S, (∀xA ⇒)S′}  \frac{S(A[t] ⇒)T}{S, (∀xA ⇒)T}  S′T′

Rule ⇒ ∀. Take the Craig interpolant as for ⇒→:

\frac{Γ, Γ′ ⇒ A[b]}{Γ, Γ′ ⇒ Δ, ∀xA, Δ′}  Γ′ ⇒ I ; exists by IH  \frac{I, Γ ⇒ A[b]}{I, Γ ⇒ Δ, ∀xA}

Rule ∃ ⇒ is excluded by the statement of the Theorem. □

In fact one can specialize interpolating formulas.

Lemma 2 If there is an interpolant for the sequents S, S′ then there is an interpolant (3) where none of I_{j} is a conjunction or disjunction.

Proof . Write (3) as

(I; T; T′)

If say I_{1} = K&L, substitute v_{1}/(v_{1}&w) with a new variable w. More precisely, replace the list v_{1}, v_{2}, …, v_{p}, by v_{1}, w, v_{2} …, v_{p}, replace the list (I_{1}, I_{2}, …, I_{p}) by (K, L, I_{2}, …, I_{p}), replace each of the sequents T_{i} ≡ v_{1}, Γ ⇒ Δ by v_{1}, w, Γ ⇒ Δ and each of the sequents T_{j} ≡ Γ ⇒ Δ, v_{1} by the pair Γ ⇒ Δ, v_{1}, Γ ⇒ Δ, w. The result of the substitution

(I_{1}; T_{1}; T′_{1})

is again an interpolant for S, S′ since the following equivalences are derivable:

&T_{1} ↔ &T[v_{1}/v_{1}&w], &T′_{1} ↔ &T′[v_{1}/v_{1}&w]

&T[v_{1}/K&L, v_{2}/I_{2}, …, v_{p}/I_{p}] ↔ &T_{1}[v_{1}/K, w/L, v_{2}/I_{2}, …, v_{p}/I_{p}]
&T′[v_{1}/K&L, v_{2}/I_{2}, …, v_{p}/I_{p}] ↔ &T′_{1}[v_{1}/K, w/L, v_{2}/I_{2}, …, v_{p}/I_{p}]

Indeed, inconsistency of conjunction of the T -part and derivability of the sequents (4) is preserved.

In the case of disjunction, I_{1} = K ∨ L, substitute v_{1}/(v_{1} ∨ w) for a new variable w. □

Let us prove that the restriction in the previous theorem is necessary: there is no interpolant for

S ≡ ∃x(P x&(Qx → r) ⇒ r;  S′ ≡ ∀x(P x → Qx ∨ r′) ⇒ r′  (9)

i.e. for the partition ∃x(P x&(Qx → r)); ∀x(P x → Qx ∨ r′) ⇒ r; r′ or

E; A ⇒ r; r′

for short. We prove there is no interpolant even for the partition

E, K; K, A ⇒ r; r′ where K ≡ P c&Qc

Assume there is an interpolant I; T; T′, and hence

(E, K ⇒ r)T^{∗},  (K, A ⇒ r′)T^{′∗},  TT′ ⊢ ∅  (10)

are derivable. The last of these relations implies that at least one of the sequents in T, T′ is positive. Since it is obvious that there is no interpolant with I in ⊤, ⊥, it is sufficient to reduce the situation to that case.

Case 1. At least one of sequents in T′ is positive, say T_{m} ≡⇒ v_{1}, …, v_{n}. Then A ⊢ I_{1} ∨ … ∨ I_{n} ∨ r′ in the standard one-succedent version of the intuitionistic predicate logic.

If the last rule in the derivation (up to admissible permutation of inferences) is ∨-succedent, then A, K ⊢ I_{j} for some j, since A, K ⇒ r′ is not even classically valid. Substituting r′/⊤ one has K ⊢ I_{j}. Since K is an antecedent term in both parts of the partition, I_{j} can be replaced by ⊤, as required. Indeed, from (10) one has

(E, K ⊢ r)T̃, (A, K ⊢ r′)T̃′, T, T′ ⊢ ∅

where T̃ ≡ T [v_{1}/I_{1}, …, v_{i}/⊤, …, v_{p}/I_{p}], i.e. with I_{j} replaced by ⊤.

Otherwise (up to elimination of redundancies) the last steps of the derivation of A ⇒ I_{1} ∨ … ∨ I_{n} ∨ r′ analyze A and K by the antecedent rules:

\frac{\frac{A, Γ, (P a → Qa ∨ r′) ⇒ P a \frac{A, Γ, Qa ⇒ G A, Γ, r′ ⇒ G}{A, Γ, Qa ∨ r′ ⇒ G}}{A, Γ, (P a → Qa ∨ r′) ⇒ G}}{{… \atop A, K ⇒ G}}

where Γ ≡ P c, Qc, (P a_{1} → Qa_{1} ∨ r′), …, (P a_{l} → Qa_{l} ∨ r′). If a ≢ c then setting r′ = ⊤ in the leftmost upper sequent, we see that it is not classically valid. If a ≡ c then the uppermost ∨-antecedent rule is redundant, since the side formula Qa is already contained in Γ.

Case 2. One of the sequents in T is positive, say T_{1} ≡⇒ v_{1}, …, v_{n}. Then ⊢ E ⊢ I_{1} ∨ … ∨ I_{n} ∨ r. By the disjunction property (Harrop theorem) E ⊢ r (which is false) or E ⊢ I_{j} for some j. Substituting r′/⊤ one has K ⇒ I_{j} and again I_{j} can be replaced by ⊤.

3 An Interpolation Theorem for Multiple Succedent Sequents

In this section we present a property of multiple-succedent sequents which implies Craig interpolation and admits a proof by induction on a derivation in multiple-succedent version of the intuitionistic predicate logic (cf. [1],[2]). Let us remind that the rules of this version coincide with corresponding classical rules with two exceptions

\frac{Γ ⇒ A[b]}{Γ ⇒ Δ, ∀xA}  \frac{Γ, A ⇒ B}{Γ ⇒ Δ, A → B}

The definition below is motivated as follows. The standard proof of Craig interpolation theorem (cf. [12]) is done by induction on derivation in one-succedent formulation say LJ of the intuitionistic predicate calculus. At this moment there seems to be no hope to find a formulation working for multiple-succedent system say LJm. At the same time, any derivation in LJm is naturally divided into parts ending in one-succedent sequents (for which usual Craig interpolation is meaningful). Among these one-succedent sequents there are premises of the rules for →, ∀-succedent. Multiple formulas in the succedent arise (if the rules are viewed bottom-up) as the results of →-antecedent inferences like

\frac{Γ ⇒ G, A Γ, B ⇒ G}{Γ, A → B ⇒ G}

If one could revert all such inferences, it would be possible to rely on Craig interpolants. We define a property S ∈ I_{n} for sequents

S ≡ Γ; Γ′ ⇒ A_{1}, …, A_{n}; Δ′  (11)

or rather for partition of S into Γ ⇒ A_{1}, …, A_{n} and Γ′ ⇒ Δ′. Notation A_{[k,n]} stands for A_{k}, …, A_{n} and A_{[k,n]−i} stands for A_{[k,i−1]}, A_{[i+1,n]}.

Definition 4

Γ; Γ′ ⇒ Δ′ ∈ I_{0} iff there is an I ∈ L_{Γ} ∩ L_{Γ′,Δ′} such that Γ ⊢ I and I, Γ′ ⊢ Δ′

For n > 0

Γ; Γ′ ⇒ A_{[1,n]}; Δ′ ∈ I_{n}

iff for every i (1 ≤ i ≤ n) and for every formula B ∈ L_{Γ,A_{[1,n]}} such that Γ, B, Γ′ ⊢ A_{[1,n]−i}, Δ′ one has

Γ, A_{i} → B; Γ′ ⇒ A_{[1,n]−i}; Δ′ ∈ I_{n−1}

Theorem 2 If Γ; Γ′ ⊢ A_{[1,n]}; Δ′ then Γ; Γ′ ⇒ A_{[1,n]}; Δ′ ∈ I_{n}

In particular, if Γ; Γ′ ⊢ Δ′ then there exists a Craig interpolant I : Γ ⊢ I, I, Γ′ ⇒ Δ′

Let us prove an extension of the Theorem 2.

Theorem 3 Let a derivation d be given ending in the following series of contractions and →-antecedent rules traceable to (A → B)_{[1,n]} in the final sequent (up to a permutation of [1, n]).

\frac{\frac{d_{2}^{+} d_{2} Γ, B_{2}, (A → B)_{[3,n]}; Γ′ ⇒ A_{1}, Δ′}{d_{1}^{+} Γ, (A → B)_{[2,n]}; Γ′ ⇒ A_{1}; Δ′} d_{1} Γ, B_{1}, (A → B)_{[2,n]}; Γ′ ⇒ Δ′}{d Γ, (A → B)_{[1,n]}; Γ′ ⇒ Δ′}

where d_{2}^{+} is

\frac{d_{0} Γ; Γ′ ⇒ A_{[1,n]}; Δ′ d_{n} Γ, B_{n}; Γ′ ⇒ A_{[1,n−1]}; Δ′}{d_{n}^{+} Γ, (A_{n} → B_{n}); Γ′ ⇒ A_{[1,n−1]}; Δ′}

…

d_{2}^{+} Γ, (A → B)_{[3,n]}; Γ′ ⇒ A_{1}, A_{2}; Δ′

Then

Γ, (A → B)_{[1,n]}; Γ′ ⇒ Δ′ ∈ I_{0}

Proof . We assume that all principal formulas in axioms are atomic and use induction on (∥d_{0}∥, Σ_{i}∥d_{i}∥, n), i.e. on

α(d^{+}) ≡ ω^{2}∥d_{0}∥ + ωΣ_{i}∥d_{i}∥ + n

where ∥d∥ is the total number of rules in d.

Induction base for ∥d_{0}∥: the sequent Γ; Γ′ ⇒ A_{[1,n]}; Δ′ is an axiom. The case when the antecedent contains ⊥ is obvious. Assume that the antecedent and succedent share an atomic formula C. If both occurences of C are in Γ′ ⇒ Δ′ then the interpolant I is ⊤. If one C is in Γ and the other is in Δ′ then I = C.

It remains to consider the situation when the antecedent occurence of C is in Γ, Γ′, and the second C is A_{i}.

Case 1. i = 1. Let I_{1} be an interpolant for d_{1}, i.e. for the sequent Γ, B_{1}, (A → B)_{[2,n]}; Γ′ ⇒ Δ′. Then if C ∈ Γ, set I ≡ I_{1}. If C ∈ Γ′, then set I ≡ (C → I_{1}).

Case 2. i > 1. Take i = n to simplify notation, and consider a new derivation:

\frac{S_{1} \frac{{d̃_{n}^{+} = d_{n} Γ, B_{n}; Γ′ ⇒ A_{[1,n−1]}; Δ′ \atop …} ; d̃_{1}^{+} S_{2} d̃_{1} Γ, B_{1}, (A → B)_{[2,n−1]}, B_{n}; Γ′ ⇒ Δ′}{d̃ Γ, (A → B)_{[1,n−1]}, B_{n}; Γ′ ⇒ Δ′}}{Γ, (A → B)_{[1,n−1]}, C → B_{n}; Γ′ ⇒ Δ′}

Here

S_{1} ≡ Γ, (A → B)_{[1,n−1]}; Γ′ ⇒ C; Δ′, S_{2} ≡ Γ, (A → B)_{[2,n−1]}, B_{n}; Γ′ ⇒ A_{1}; Δ′

and d̃ denotes the result of replacing all predecessors of (C → B_{n}) in d by B_{n} and deleting corresponding →-antecedent inferences. Note that α(d̃) < α(d) since at least one such inference is eliminated, and hence IH is applicable to d̃. Now use case 1.

In the inductition step for ∥d_{0}∥ consider cases depending of the last rule R in d_{0}.

Case 3. The principal formula of R is in Γ, Γ′, Δ′ and R is not →-antecedent with principal formula in Γ. Then R can be permuted to become the last rule, and IH will be applicable to its premises. Now the interpolant for the conclusion is obtained from interpolants for the premises in the standard way.

Case 4. R is →-antecedent with the principal formula in Γ:

\frac{d_{0}^{−} Γ; Γ′ ⇒ A_{[0,n]}; Δ′ Γ, B_{0}; Γ′ ⇒ A_{[1,n]}; Δ′}{d_{0} Γ, A_{0} → B_{0}; Γ′ ⇒ A_{[1,n]}; Δ′}

Here ∥d_{0}^{−}∥ < ∥d_{0}∥, and IH is applicable.

Case 5. The principal formula of R is one of A_{i}, say A_{1}.

Case 5.1. A_{1} ≡ ∀xA, i.e. there exist I_{1}, I_{2} such that:

R \frac{Γ, Γ′ ⇒ A[b]}{Γ, Γ′ ⇒ ∀xA, A_{[2,n]}, Δ′} \begin{matrix}Γ′ ⊢ I_{1}, I_{1}, Γ ⊢ A[b] \\ Γ, (A → B)_{[2,n]}, B_{1} ⊢ I_{2} & I_{2}, Γ′ ⊢ Δ′ \end{matrix}

Hence ∀xI_{1}[b/x] → I_{2} is an interpolant for the conclusion of R:

\frac{Γ, (A → B)_{[2,n]}, ∀xA → B_{1}, ∀xI_{1}[b/x] ⊢ I_{2}}{Γ, (A → B)_{[2,n]}, ∀xA → B_{1} ⊢ ∀xI_{1}[b/x] → I_{2}} \frac{Γ′ ⊢ ∀xI_{1}[b/x], Δ′ I_{2}, Γ′ ⊢ Δ′}{∀xI_{1}[b/x] → I_{2}, Γ′ ⊢ Δ′}

Case 5.2. A_{1} ≡ C → D. Similar to the previous case. The interpolant is I_{1} → I_{2}.

Case 5.3. A_{1} ≡ ∃xA. Use IH and the implication ∃xA → B_{1} ⊢ A[t] → B_{1}. Case 5.4. A_{1} ≡ B ∨ C. Use IH and the implication: (B ∨ C → B_{1}) ⊢ (B →

B_{1})&(C → B_{1})

Case 5.5. A_{1} ≡ B&C. Use IH and the implication (B&C) → B_{1} ≡ B → (C → B_{1}) □

4 Kripke-style System

As pointed out in the introduction, one of the motivations for this work was a formulation suitable for a version first stated in [6] (and independently by [7]). This version derives tableaux, i.e. sequents consisting of indexed formulas σA, where the index σ is a finite sequence of natural numbers and A is a formula. Indices are interpreted as possible worlds with accessibility relation Rσσ′ ≡ (σ′ = σ ∗ τ) for some τ. Kripke defined a translation of tableaux into formulas, but it is not clear how to use it for our purposes, since this translation intermixes the parts of the tableau traceable to the premise and the conclusion of the original interpolation problem.

A formulation similar to Theorem 2 can be obtained using the transformation of tableau derivations into sequent derivations described below. It is still not clear how to obtain more perspicuous interpolation theorem for tableaux.

4.1 System KInt

Let us recall the typical rules of tableau formulation as presented in [8] (and in [9] for the modal case). In most cases we group all formulas with one and the same index σ together and write a tableau in the form U; σS, where S is a sequent, U is the remaining part of the tableau.

Axioms: U; σ A, Γ → Δ, A

Inference rules

(& ⇒) \frac{U; σA, B, Γ ⇒ Δ}{U; σ(A&B), Γ ⇒ Δ}  \frac{U; σΓ ⇒ Δ, A  U; σΓ ⇒ Δ, B}{U; σΓ ⇒ Δ, (A&B)} (& ⇒)

(→⇒) \frac{U; σΓ ⇒ Δ, A U; σB, Γ ⇒ Δ,}{U; σA → B, Γ ⇒ Δ}  \frac{U; σΓ ⇒ Δ; (σ ∗ i)A, Γ ⇒ B}{U; σΓ ⇒ Δ, A → B} (⇒→)

(transfer)\frac{U; σA, Γ ⇒ Δ; (σ ∗ i)A, Γ′ ⇒ Δ′}{U; σA, Γ ⇒ Δ; (σ ∗ i)Γ′ ⇒ Δ′}

Lemma 3 If the transfer rule is not used in a derivation d of a tableau

d : σ_{1}S_{1}; …; σ_{n}S_{n}

then d can be pruned to a derivation of a sequent σ_{i}S_{i} in the multiple-succedent sequent system LJm.

Proof . Use induction on d. □

Definition 5 The rules ⇒→, ⇒ ∀ which give rise to new indices are called non-invertible, all other rules are invertible

An invertible inference with the principal sequent σS is normal if there is no index τ with Rστ in the same tableau.

Lemma 4 If all invertible inferences in a derivation d are normal then d can be pruned to a derivation in LJm

Proof . We use induction on d. Induction base is obvious, consider induction step. For a tableau T and a sequent σΓ → Δ occurring in T let σ̃ ≡ Γ_{≤σ} → Δ, where Γ_{≤σ} is the union of antecedents of all sequents τS′ occuring in T with Rτσ.

We prove that d can be pruned to a derivation of a sequent of the form σ̃ where σ is one of the maximal indices in the last tableau T of d (i.e. there is no τ in T with Rστ). In other words, we add implicitly applications of the transfer rule. Consider cases depending on the last rule R of d. By IH every premise of R can be pruned to one of its components If at least one of these components (in the case of a two-premise rule) is not principal in the conclusion, then the conclusion is pruned to the same component. Otherwise, T is pruned to its principal component wich is derived by the rule R (except transfer rule which disappears). □

Lemma 5 Every derivation in KInt can be transformed (by permuting invertible inferences down) into a derivation of the same tableau where all invertible inferences are normal.

Proof . Routine (cf. [4]), long.

4.2 Analytic Cut

A cut-inference

\frac{Γ ⇒ Δ, A A, Σ ⇒ Π}{Γ, Σ ⇒ Δ, Π}

is analytic if A is a subformula of the conclusion. Note that the standard proof of the intepolation theorem by induction on a Gentzen-type derivation still goes through in the presence of the analytic cut. In the intuitionistic case Δ should be empty. A method to transform tableau formulations of modal logics into a sequent formulation with analytic cut is presented in [10].

References

[1] Beth E.W., Semantic Construction of Intuitionistic Logic, Med. Kon. Nederl. Akad. Wetensch., 19, 1956, 357-388

[2] Curry H.B., Foundations of Mathematical Logic, McGraw-Hill, NY, 1963

[3] Craig W., Linear Reasoning, JSL, 22, 1957, 250-268

[4] Kleene S.C., Permutability of inferences in Gentzen’s Calculi LK and LJ, Memoirs Amer. Math. Soc., 1952, no. 10, 1-26

[5] Kleene S.C., Mathematical Logic, John Wiley and Sons, NY, 1967

[6] Kripke S. , Semantical analysis of intuitionistic logic I. in: Formal Systems and Recursive Functions, Amsterdam, North-Holland, 1965, 92-130

[7] Maslov S.Ju., An invertible sequent variant of the constructive predicate calculus,(Russian) A.O.Slisenko (editor). Zapiski Nauchnykh Seminarov LOMI. v.4, 1967, 96-111; English translation in: Seminars in Mathematics, V.A. Steklov Math. Inst., Plenum Publishers, 1969, 4,

[8] Mints G., Varying of Proof-search Tactics in Sequenzen-Calculi. Seminars in Mathematics, V.A. Steklov Math. Inst., Plenum Publishers, 1969, 4, 52-69

[9] Mints G.,Indexed systems of sequents and cut-elimination, Journal of Philosophical Logic, v. 26, no 6, 1997, p. 671-696

[10] Mints G., Analytic Cut in Modal Logic (Russian). Soviet Conference in Applied Logic, Novosibirsk, 1985, 141-142

[11] Maksimova L. Interpolation properties of super-intuitionistic logics, Studia Logica, 38, 1979, 419-428

[12] Schütte K. Der Interpolationssatz der intuitionistischen Prädikatenlogik, Math. Ann., 148, 1962, 192-200