Craig's interpolation theorem for modal logics

In [1] Craig introduced a proof procedure for first order classical logic called linear reasoning. In it, a proof of P ⊃ Q consists of a sequence of formulas, each of which implies the next, beginning with P and ending with Q. And one of the formulas in the sequence will be an interpolation formula for P ⊃ Q. Indeed, this was the first proof of the Craig interpolation theorem, some of whose important consequences were demonstrated in a companion paper [2]. In this paper we present systems of linear reasoning for several standard modal logics: K, T, K4, S4, D, D4, and GL. Similar systems can be constructed for several regular, nonnormal modal logics too, though we do not do so here. And just as in the classical case, interpolation theorems are easy consequences. Such theorems are well known for the logics considered here. There is a model theoretic argument in [6], an argument using Gentzen systems in [8], an argument using consistency properties in [4] and [5], and an argument using symmetric Gentzen systems in [5]. This paper presents what seems to be the first modal proof that follows Craig's original methods. We note that if the modal rules given here are dropped, a classical linear reasoning system results, which is related to, but not the same as those in [1] and [10].Since the basic linear reasoning ideas are fully illustrated by the propositional case, we present that first, to keep the clutter down. Later we show how the techniques can generally be extended to encompass quantifiers. We do not follow [1] in making heavy use of prenex form, since it is not generally available in modal logics. Fortunately, it plays no essential role.

Download Full-text

On weak and strong interpolation in algebraic logics

Journal of Symbolic Logic ◽

10.2178/jsl/1140641164 ◽

2006 ◽

Vol 71 (1) ◽

pp. 104-118 ◽

Cited By ~ 12

Author(s):

Gábor Sági ◽

Saharon Shelah

Keyword(s):

Algebraic Logic ◽

Amalgamation Property ◽

Weak Form ◽

Interpolation Theorem ◽

Order Logic ◽

Cylindric Algebras ◽

First Order ◽

Finite Dimensional ◽

Craig’S Interpolation Theorem ◽

Superamalgamation Property

AbstractWe show that there is a restriction, or modification of the finite-variable fragments of First Order Logic in which a weak form of Craig's Interpolation Theorem holds but a strong form of this theorem does not hold. Translating these results into Algebraic Logic we obtain a finitely axiomatizable subvariety of finite dimensional Representable Cylindric Algebras that has the Strong Amalgamation Property but does not have the Superamalgamation Property. This settles a conjecture of Pigozzi [12].

Download Full-text

Interpolation theorems for Lk,k2+

Journal of Symbolic Logic ◽

10.2307/2273530 ◽

1978 ◽

Vol 43 (3) ◽

pp. 535-549 ◽

Cited By ~ 1

Author(s):

Ruggero Ferro

Keyword(s):

Natural Deduction ◽

Interpolation Theorem ◽

Positive Answer ◽

Strong Limit ◽

First Order ◽

Limit Cardinal ◽

Saturated Models ◽

Order Language ◽

Craig’S Interpolation Theorem

Chang, in [1], proves an interpolation theorem (Theorem I, remark b)) for a first-order language. The proof of Chang's theorem uses essentially nonsimple devices, like special and ω1-saturated models.In remark e) in [1], Chang asks if there is a simpler proof of his Theorem I.In [1], Chang proves also another interpolation theorem (Theorem II), which is not an extension of his Theorem I, but extends Craig's interpolation theorem to Lα+,ω languages with interpolant in Lα+,α where α is a strong limit cardinal of cofinality ω.In remark k) in [1], Chang asks if there is a generalization of both Theorems I and II in [1], or at least a generalization of both Theorem I in [1] and Lopez-Escobar's interpolation theorem in [7].Maehara and Takeuti, in [8], show that there is a completely different proof of Chang's interpolation Theorem I as a consequence of their interpolation theorems. The proofs of these theorems of Maehara and Takeuti are proof theoretical in character, involving the notion of cut-free natural deduction, and it uses devices as simple as those needed for the usual Craig's interpolation theorem. Hence this can be considered as a positive answer to Chang's question in remark e) in [1].

Download Full-text

Interpolation for first order S5

Journal of Symbolic Logic ◽

10.2178/jsl/1190150101 ◽

2002 ◽

Vol 67 (2) ◽

pp. 621-634 ◽

Cited By ~ 11

Author(s):

Melvin Fitting

Keyword(s):

Interpolation Theorem ◽

Modal Logics ◽

First Order ◽

Propositional Quantifiers

AbstractAn interpolation theorem holds for many standard modal logics, but first order S5 is a prominent example of a logic for which it fails. In this paper it is shown that a first order S5 interpolation theorem can be proved provided the logic is extended to contain propositional quantifiers. A proper statement of the result involves some subtleties, but this is the essence of it.

Download Full-text

Back and forth constructions in modal logic: An interpolation theorem for a family of modal logics

Journal of Symbolic Logic ◽

10.2307/2273909 ◽

1986 ◽

Vol 51 (4) ◽

pp. 969-980 ◽

Cited By ~ 3

Author(s):

George Weaver ◽

Jeffrey Welaish

Keyword(s):

Modal Logic ◽

Logical Consequence ◽

Logical Truth ◽

Interpolation Theorem ◽

Modal Logics ◽

Kripke Semantics ◽

Direct Products ◽

Possible World ◽

Relational Systems ◽

Modal Analogue

The following is a contribution to the abstract study of the model theory of modal logics. Historically, individual modal logics have been specified deductively; and, as a result, it has seemed natural to view modal logics as sets of sentences provable in some deductive system. This proof theoretic view has influenced the abstract study of modal logics. For example, Fine [1975] defines a modal logic to be any set of sentences in the modal language L□ which contains all tautologies, all instances of the schema (□(ϕ ⊃ Ψ) ⊃ (□ϕ ⊃ □Ψ)), and which is closed under modus ponens, necessitation and substitution.Here, however, modal logics are equated with classes of “possible world” interpretations. “Worlds” are taken to be ordered pairs (a, λ), where a is a sentential interpretation and λ is an ordinal. Properties of the accessibility relation are identified with those classes of binary relational systems closed under isomorphisms. The origin of this approach is the study of alternative Kripke semantics for the normal modal logics (cf. Weaver [1973]). It is motivated by the desire that modal logics provide accounts of both logical truth and logical consequence (cf. Corcoran and Weaver [1969]) and the realization that there are alternative Kripke semantics for S4, B and M which give identical accounts of logical truth, but different accounts of logical consequence (cf. Weaver [1973]). It is shown that the Craig interpolation theorem holds for any modal logic which has characteristic modal axioms and whose associated class of binary relational systems is closed under subsystems and finite direct products. The argument uses a back and forth construction to establish a modal analogue of Robinson's theorem. The argument for the interpolation theorem from Robinson's theorem employs modal analogues of the Ehrenfeucht-Fraïssé characterization of elementary equivalence and Hintikka's distributive normal form, and is itself a modal analogue of a first order argument (cf. Weaver [1982]).

Download Full-text