Atlas: Interpolation Theorems for Intuitionistic Predicate Logic by Grigori Mints

Atlas home || Conferences | Abstracts | about Atlas

First St.Petersburg Days of Logic and Computability
May 26-29, 1999
Steklov Institute of Mathematics
St. Petersburg, Russia

Organizers
Evgeny Dantsin, Gennadii Davydov, Dima Grigoriev, Eduard Karavaev, Nickolai Kossovskii, Vladimir Lifschitz, Maurice Margenstern, Yuri Matiyasevich (chairman), Grigori Mints, Vladimir Orevkov, Anatol Slissenko, Maxim Vsemirnov

View Abstracts
Conference Homepage

Interpolation Theorems for Intuitionistic Predicate Logic
by
Grigori Mints
Dept. of Philosophy, Stanford University

Interpolation Theorems for Intuitionistic Predicate Logic

G. Mints
Dept. of Philosophy, Stanford Univ., Stanford, CA 94305, USA

1 Propositional Interpolation

Craig interpolation theorem (which holds for intuitionistic logic) implies that the derivability of \Gamma, \Gamma' ===> \Delta' implies existence of a Craig interpolant I in the common language of \Gamma and \Gamma' ===> \Delta' such that both \Gamma ===> I and I, \Gamma' ===> \Delta' are derivable. For classical logic this extends to the partition \Gamma;\Gamma' ===> \Delta;\Delta', i.e. there is an interpolant I satisfying \Gamma ===> \Delta, I and I, \Gamma' ===> \Delta'. For intuitionistic logic the partition ;C ===> C; is a counterexample.

Nevertheless some interpolation properties for disjunction are true also in the intuitionistic case. We present here a multiple-succedent version of interpolation true for intuitionistic propositional (but not for predicate) logic. Similar result was established earlier by L. Maksimova [4]. More complicated version holds for the predicate case. L_E denotes below the language of the expression (formula, sequent etc.) E, and \Gamma\vdash\Delta indicates that the sequent \Gamma ===> \Delta is intuitionistically derivable.

Definition. Let v₁, ... , v_p be distinct propositional variables and

T₁;T₂; ... ;T_k k >= 2
(1)
be sequents with distinct antecedent and succedent terms all among v₁, ... , v_p, for example

v₂, v₃ ===> v₁, v₄; ===> v₂; ===> v₃; v₁ ===> ; v₄ ===>

We say that (1) is balanced iff it is classically inconsistent. Note that by the completeness of the resolution rule (1) is balanced iff the empty sequent ===> is derivable from (1) by a series of cuts.

If S \equiv \Gamma ===> \Delta, S' \equiv \Gamma' ===> \Delta' then (following [2]) SS' \equiv \Gamma, \Gamma' ===> \Delta, \Delta'. Classically SS' corresponds to S \/ S'.

Definition. Let S, S' be arbitrary sequents, I₁, ... , I_p be formulas, v₁, ... , v_p be distinct new propositional variables, and (1) be a list of sequents composed from v₁, ... , v_p. We say that

(I₁, ... , I_p;T₁; ... ;T_k)
(2)
is an interpolant for S, S' iff all predicate symbols of I₁, ... , I_p are common to S and S', the list T₁; ... ;T_k is balanced and there is an m (1 <= m < k) such that all sequents

ST₁^*, ... , ST_m^*, S'T_m+1^*, ... , S'T_k^*

are derivable, where T^*=T[v₁/I₁, ... , 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

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

The restriction in the previous theorem is necessary: there is no interpolant for

S \equiv existsx(Px & (Qx --> r) ===> r; S' \equiv for allx(Px --> Qx \/ r') ===> r'

2 An Interpolation Theorem for Multiple Succedent Sequents

The definition below is motivated as follows. The standard proof of Craig interpolation theorem (cf. [5]) 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 --> , for all-succedent. Multiple formulas in the succedent arise (if the rules are viewed bottom-up) as the results of --> -antecedent inferences like

\Gamma ===> G, A \Gamma, B ===> G

\Gamma, A --> B ===> G

If one could revert all such inferences, it would be possible to rely on Craig interpolants. We define a property S in I _n for sequents

S \equiv \Gamma;\Gamma' ===> A₁, ... , A_n;\Delta'

(3)

or rather for partitions of S into \Gamma ===> A₁, ... , A_n and \Gamma' ===> \Delta'. 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

\Gamma;\Gamma' ===> \Delta' in I ₀ iff there is an I in L_\Gamma \cap L_{\Gamma', \Delta'} such that \Gamma\vdash I and I, \Gamma'\vdash \Delta'

\Gamma;\Gamma' ===> A_{[1, n]};\Delta' in I _n (n > 0)

iff for every i (1 <= i <= n) and for every formula B in L_{\Gamma, A_{[1, n]}}

\Gamma, B, \Gamma'\vdash A_{[1, n]-i}, \Delta' implies \Gamma, A_i --> B;\Gamma' ===> A_{[1, n]-i};\Delta' in I _n-1

Theorem 2 If \Gamma;\Gamma'\vdash A_{[1, n]};\Delta' then \Gamma;\Gamma' ===> A_{[1, n]};\Delta' in I _n

In particular, if \Gamma;\Gamma'\vdash \Delta' then there exists a Craig interpolant I:

\Gamma\vdash I, I, \Gamma' ===> \Delta'

References

[]: . Kleene S.C., Permutability of inferences in Gentzen's Calculi LK and LJ, Memoirs Amer. Math. Soc., 1952, no. 10, 1-26
[]: . Kleene S.C., Mathematical Logic, John Wiley and Sons, NY, 1967
[]: . Maksimova L. Interpolation properties of super-intuitionistic logics, Studia Logica, 38, 1979, 419-428
[]: . Schütte K. Der Interpolationssatz der intuitionistischen Prädikatenlogik, Math. Ann., 148, 1962, 192-200

Date received: April 3, 1999

Interpolation Theorems for Intuitionistic Predicate Logic

G. Mints Dept. of Philosophy, Stanford Univ., Stanford, CA 94305, USA

1 Propositional Interpolation

2 An Interpolation Theorem for Multiple Succedent Sequents

References

G. Mints
Dept. of Philosophy, Stanford Univ., Stanford, CA 94305, USA