We present a number of, somewhat unusual, ways of describing what Craig’s interpolation theorem achieves, and use them to identify some open problems and further directions.

We prove the following surprising property of Heyting's intuitionistic propositional calculus, IpC. Consider the collection of formulas, φ, built up from propositional variables (p,q,r,...) and falsity $(\perp)$ using conjunction $(\wedge)$ , disjunction (∨) and implication (→). Write $\vdash\phi$ to indicate that such a formula is intuitionistically valid. We show that for each variable p and formula φ there exists a formula Apφ (effectively computable from φ), containing only variables not equal to p which occur in φ, and such that for (...) all formulas ψ not involving $p, \vdash \psi \rightarrow A_p\phi$ if and only if $\vdash \psi \rightarrow \phi$ . Consequently quantification over propositional variables can be modelled in IpC, and there is an interpretation of the second order propositional calculus, IpC2, in IpC which restricts to the identity on first order propositions. An immediate corollary is the strengthening of the usual interpolation theorem for IpC to the statement that there are least and greatest interpolant formulas for any given pair of formulas. The result also has a number of interesting consequences for the algebraic counterpart of IpC, the theory of Heyting algebras. In particular we show that a model of IpC2 can be constructed whose algebra of truth-values is equal to any given Heyting algebra. (shrink)

In this paper we investigate the connections between quantifier elimination, decidability and Uniform Craig Interpolation in Δ-core fuzzy logics added with propositional quantifiers. As a consequence, we are able to prove that several propositional fuzzy logics have a conservative extension which is a Δ-core fuzzy logic and has Uniform Craig Interpolation.

In our previous paper [5], we have studied Kripke-type semantics for propositional logics without the contraction rule. In this paper, we will extend our argument to predicate logics without the structure rules. Similarly to the propositional case, we can not carry out Henkin's construction in the predicate case. Besides, there exists a difficulty that the rules of inference () and () are not always valid in our semantics. So, we have to introduce a notion of normal models.

This paper shows a role of the contraction rule in decision problems for the logics weaker than the intuitionistic logic that are obtained by deleting some or all of structural rules. It is well-known that for such a predicate logic L, if L does not have the contraction rule then it is decidable. In this paper, it will be shown first that the predicate logic FLec with the contraction and exchange rules, but without the weakening rule, is undecidable while the (...) propositional fragment of FLec is decidable. On the other hand, it will be remarked that logics without the contraction rule are still decidable, if our language contains function symbols. (shrink)

We show that (contrary to the parallel case of intuitionistic logic, see [7], [4]) there does not exist a translation fromS42 (the propositional modal systemS4 enriched with propositional quantifiers) intoS4 that preserves provability and reduces to identity for Boolean connectives and.

A. M. Pitts in [Pi] proved that HA op fp is a bi-Heyting category satisfying the Lawrence condition. We show that the embedding $\Phi: HA^\mathrm{op}_\mathrm{fp} \longrightarrow Sh(\mathbf{P_0,J_0})$ into the topos of sheaves, (P 0 is the category of finite rooted posets and open maps, J 0 the canonical topology on P 0 ) given by $H \longmapsto HA(H,\mathscr{D}(-)): \mathbf{P_0} \longrightarrow \text{Set}$ preserves the structure mentioned above, finite coproducts, and subobject classifier, it is also conservative. This whole structure on HA op (...) fp can be derived from that of Sh(P 0 ,J 0 ) via the embedding Φ. We also show that the equivalence relations in HA op fp are not effective in general. On the way to these results we establish a new kind of duality between HA op fp and a category of sheaves equipped with certain structure defined in terms of Ehrenfeucht games. Our methods are model-theoretic and combinatorial as opposed to proof-theoretic as in [Pi]. (shrink)

The purpose of this paper is to connect the proof theory and the model theory of a family of propositional logics weaker than Heyting's. This family includes systems analogous to the Lambek calculus of syntactic categories, systems of relevant logic, systems related toBCK algebras, and, finally, Johansson's and Heyting's logic. First, sequent-systems are given for these logics, and cut-elimination results are proved. In these sequent-systems the rules for the logical operations are never changed: all changes are made in the structural (...) rules. Next, Hubert-style formulations are given for these logics, and algebraic completeness results are demonstrated with respect to residuated lattice-ordered groupoids. Finally, model structures related to relevant model structures (of Urquhart, Fine, Routley, Meyer, and Maksimova) are given for our logics. These model structures are based on groupoids parallel to the sequent-systems. This paper lays the ground for a kind of correspondence theory for axioms of logics with implication weaker than Heyting's, a correspondence theory analogous to the correspondence theory for modal axioms of normal modal logics.The first part of the paper, which follows, contains the first two sections, which deal with sequent-systems and Hubert-formulations. The second part, due to appear in the next issue of this journal, will contain the third section, which deals with groupoid models. (shrink)

We discuss the interpolation property on some important families of non classical logics, such as intuitionistic, modal, fuzzy, and linear logics. A special paragraph is devoted to a generalization of the interpolation property, uniform interpolation.

We investigate uniform interpolants in propositional modal logics from the proof-theoretical point of view. Our approach is adopted from Pitts’ proof of uniform interpolationin intuitionistic propositional logic [15]. The method is based on a simulation of certain quantifiers ranging over propositional variables and uses a terminating sequent calculus for which structural rules are admissible.

The paper deals with a rst order intuitionistic predicate calculus with- out contraction. We examine the Hilbert variant of this calculus and an equivalent Genzen variant of it, prove that this calculus is decidable, evalu- ate its complexity of deduction and study its connection with the classical logics.