pith. sign in

arxiv: 2604.02082 · v2 · submitted 2026-04-02 · 🧮 math.LO

Fischer-Servi logic does not have interpolation

Rodrigo Nicolau Almeida , Nick Bezhanishvili , Simon Lemal This is my paper

Pith reviewed 2026-05-13 20:51 UTC · model grok-4.3

classification 🧮 math.LO
keywords Fischer-Servi logicCraig interpolationmodal Heyting algebrasamalgamation propertyintuitionistic modal logicIK logicIT logicIS4 logic
0
0 comments X

The pith

Fischer-Servi logic IK does not have the Craig interpolation property.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that the Fischer-Servi logic IK fails the Craig interpolation property. The proof proceeds by establishing that the class of modal Heyting algebras that interpret IK lacks the amalgamation property. The same algebraic failure is shown to hold for the extensions IT, IK4, IS4 and IGL. A reader would care because interpolation guarantees that a consequence provable from two separate premises can be broken into an intermediate formula whose vocabulary is restricted to their common symbols; without it, proofs in these logics cannot be decomposed in the modular way familiar from classical or intuitionistic propositional logic.

Core claim

We prove that the Fischer-Servi logic IK does not have the Craig interpolation property. This is obtained by showing that the corresponding class of modal Heyting algebras lacks the amalgamation property. We also generalize this result to some extensions of the Fischer-Servi logic such as IT, IK4, IS4, and IGL.

What carries the argument

The class of modal Heyting algebras that interpret IK, together with the demonstration that this class fails the amalgamation property.

If this is right

  • IK does not admit Craig interpolation.
  • The corresponding modal Heyting algebras fail amalgamation.
  • The same negative result holds for the logics IT, IK4, IS4 and IGL.
  • Interpolation therefore cannot be used to decompose proofs in any of these systems.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Other intuitionistic modal logics that lack similar algebraic closure properties may also fail interpolation.
  • One could search for small finite counter-models in which an explicit interpolant is provably absent.
  • The result limits the applicability of modular proof techniques in intuitionistic modal reasoning.

Load-bearing premise

The standard translation that equates Craig interpolation in the logic with the amalgamation property in its algebraic semantics continues to hold for the modal Heyting algebras used here.

What would settle it

An explicit pair of modal Heyting algebras A and B with a common subalgebra C such that no amalgam exists over C, or a concrete pair of IK-formulas whose consequence cannot be interpolated.

Figures

Figures reproduced from arXiv: 2604.02082 by Nick Bezhanishvili, Rodrigo Nicolau Almeida, Simon Lemal.

Figure 1
Figure 1. Figure 1: Confluence conditions for Fischer-Servi By convention, horizontal arrows will correspond to R, and vertical arrows to ď. We will also use colors to assist in the distinction: R will be red, and ď will be blue. We will also need the morphisms of Fischer-Servi frames: Definition 2.5. Let f : X Ñ Y be a map between FS-frames. We say that f is an FS-morphism if: (i) f is a ď-p-morphism. (ii) If xRy, then f(x)R… view at source ↗
Figure 2
Figure 2. Figure 2: Amalgamation of algebras To prove that Craig interpolation implies the amalgamation property, we need to establish a correspondence between filters and congruences of FS-algebras: Definition 3.3. A filter F on an FS-algebra is called a modal filter if whenever a P F then a P F. Lemma 3.4. Given an FS-algebra A, there is a 1-1 correspondence between modal filters on A and congruences. Proof. It is well-know… view at source ↗
Figure 3
Figure 3. Figure 3: The co-V formation (Z, X, Y ) 8 [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
read the original abstract

We prove that the Fischer-Servi logic $\mathsf{IK}$ does not have the (Craig) interpolation property. This is obtained by showing that the corresponding class of modal Heyting algebras lacks the amalgamation property. We also generalize this result to some extensions of the Fischer-Servi logic such as $\mathsf{IT}$, $\mathsf{IK4}$, $\mathsf{IS4}$, and $\mathsf{IGL}$.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript proves that the Fischer-Servi logic IK lacks the Craig interpolation property by establishing that the corresponding class K of modal Heyting algebras fails the amalgamation property. The argument is extended to show failure of amalgamation (hence interpolation) for the extensions IT, IK4, IS4, and IGL as well.

Significance. If the counterexample constructions and the application of the algebraic correspondence hold, the result supplies a concrete negative answer for an important intuitionistic modal logic and its extensions. The algebraic route via amalgamation is a standard and effective method in the field; explicit counterexamples in K would constitute a falsifiable, checkable contribution.

major comments (2)
  1. [§3] §3 (or the section containing the main counterexample): the two modal Heyting algebras A and B are asserted to validate IK while their pushout in the larger class fails to do so. The verification that the bimodal operators satisfy the Fischer-Servi interaction axiom in A and B, and that the amalgam violates it, must be spelled out equation-by-equation; currently the check appears only sketched.
  2. [§2.2] §2.2 (algebraic semantics): the claim that K is precisely the variety of modal Heyting algebras for which IK is sound and complete relies on a cited general theorem for bimodal Heyting algebras. Because the Fischer-Servi axiom links □ and ◇ in a non-standard way, the paper should either reproduce the relevant fragment of the Blok-Pigozzi algebraizability argument or cite a reference that explicitly covers this signature.
minor comments (2)
  1. Notation for the two modal operators is occasionally overloaded; a uniform convention (e.g., □ for necessity and ◇ for possibility throughout) would improve readability.
  2. The generalization to IT, IK4, IS4, and IGL is stated in the abstract and conclusion but the explicit counterexamples for each are only indicated; a short table or paragraph listing the modified axioms and the corresponding algebras would make the extension self-contained.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and the constructive suggestions. We agree that both major comments identify places where the manuscript can be made more self-contained and explicit. We address each point below and will incorporate the necessary expansions in the revised version.

read point-by-point responses

  1. Referee: §3 (or the section containing the main counterexample): the two modal Heyting algebras A and B are asserted to validate IK while their pushout in the larger class fails to do so. The verification that the bimodal operators satisfy the Fischer-Servi interaction axiom in A and B, and that the amalgam violates it, must be spelled out equation-by-equation; currently the check appears only sketched.

    Authors: We agree that the verification of the Fischer-Servi axiom in A and B, together with its failure in the pushout, is currently only sketched. In the revised manuscript we will add a fully expanded, equation-by-equation check for each of the relevant identities, making the counterexample directly verifiable from the text. revision: yes

  2. Referee: §2.2 (algebraic semantics): the claim that K is precisely the variety of modal Heyting algebras for which IK is sound and complete relies on a cited general theorem for bimodal Heyting algebras. Because the Fischer-Servi axiom links □ and ◇ in a non-standard way, the paper should either reproduce the relevant fragment of the Blok-Pigozzi algebraizability argument or cite a reference that explicitly covers this signature.

    Authors: The algebraic semantics for IK is obtained by instantiating the general Blok-Pigozzi algebraizability theorem for bimodal Heyting algebras to the specific signature and axioms of IK. To address the referee’s concern, we will include a short, self-contained paragraph in §2.2 that reproduces the relevant fragment of the algebraizability argument, explicitly verifying that the Fischer-Servi axiom is preserved under the translation and that the resulting quasivariety is in fact a variety. revision: yes

Circularity Check

0 steps flagged

Direct negative proof via explicit counterexample for amalgamation; no reduction to inputs

full rationale

The derivation proceeds by constructing a specific class K of modal Heyting algebras validating IK, exhibiting a failure of amalgamation in K via concrete algebras and embeddings, and invoking the standard algebraic-logic correspondence (AP implies CIP) which is external to the paper's constructions. No equation or definition in the paper equates the target non-interpolation result to a fitted parameter or self-referential mapping; the counterexample is independent of the conclusion. Self-citations, if present, are not load-bearing for the central negative result.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The proof rests on the standard correspondence between Craig interpolation and amalgamation for modal Heyting algebras; no free parameters or invented entities are introduced.

axioms (2)
  • domain assumption The algebraic semantics of Fischer-Servi logic IK is given by modal Heyting algebras.
    Invoked in the abstract to link the logical property to the algebraic one.
  • domain assumption Amalgamation failure in the algebraic class implies interpolation failure in the logic.
    Standard result in algebraic logic used without further justification in the abstract.

pith-pipeline@v0.9.0 · 5353 in / 1160 out tokens · 21249 ms · 2026-05-13T20:51:41.746102+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

36 extracted references · 36 canonical work pages · 1 internal anchor

  1. [1]

    J. P. Aguilera and L. Pacheco. ‘Intuitionistic Gödel-Löb without Sharps’ . In: ACM Trans- actions on Computational Logic 26.4 (Sept. 2025), pp. 1–14. issn: 1557-945X. url: http: //dx.doi.org/10.1145/3748649

    work page doi:10.1145/3748649 2025

  2. [2]

    R. N. Almeida, N. Bezhanishvili and S. Lemal. Superamalgamation for modal lattices via non-distributive dualities . 2026. url: https://arxiv.org/abs/2602.20380

    work page arXiv 2026

  3. [3]

    Bezhanishvili

    G. Bezhanishvili. ‘Varieties of Monadic Heyting Algebras Part II: Duality Theory’ . In: Studia Logica 62.1 (Jan. 1999), pp. 21–48. issn: 1572-8730. url: http://dx.doi.org/ 10.1023/A:1005173628262

    work page doi:10.1023/a:1005173628262 1999

  4. [4]

    Bezhanishvili

    G. Bezhanishvili. ‘Varieties of Monadic Heyting Algebras. Part I’ . In: Studia Logica 61.3 (Nov. 1998), pp. 367–402. issn: 1572-8730. url: http : / / dx . doi . org / 10 . 1023 / A : 1005073905902

    work page 1998

  5. [5]

    Bezhanishvili

    G. Bezhanishvili. ‘Varieties of Monadic Heyting Algebras. Part III’ . In: Studia Logica 64.2 (Feb. 2000), pp. 215–256. issn: 1572-8730. url: http : / / dx . doi . org / 10 . 1023 / A : 1005285631357

    work page 2000

  6. [6]

    Bezhanishvili, B

    N. Bezhanishvili, B. ten Cate and R. Iemhoff. ‘Six Proofs of Interpolation for the Modal Logic K’ . In: Theory and Applications of Craig Interpolation . Ed. by B. ten Cate et al. Ubiquity Press, 2026

    work page 2026

  7. [7]

    Blackburn, M

    P. Blackburn, M. de Rijke and Y. Venema. Modal logic. Vol. Cambridge tracts in theor- etical computer science. 53. Cambridge, England: Cambridge University Press, 2002

    work page 2002

  8. [8]

    ten Cate et al

    B. ten Cate et al. Theory and Applications of Craig Interpolation . Ubiquity Press, 2026. url: https://cibd.bitbucket.io/taci/. 11

    work page 2026

  9. [9]

    Chagrov and M

    A. Chagrov and M. Zakharyaschev. Modal Logic. Oxford Logic Guides. Oxford, England: Clarendon Press, 1997

    work page 1997

  10. [10]

    J. Czermak. ‘Interpolation Theorem for Some Modal Logics’ . In: Logic Colloquium ’73 . Ed. by H. Rose and J. Shepherdson. Vol. 80. Studies in Logic and the Foundations of Mathematics. Elsevier, 1975, pp. 381–393. url: https : / / www . sciencedirect . com / science/article/pii/S0049237X08719578

    work page 1975

  11. [11]

    A. Das, I. van der Giessen and S. Marin. ‘Intuitionistic Gödel-Löb Logic, à la Simpson: Labelled Systems and Birelational Semantics’ . en. In: vol. 288. Schloss Dagstuhl – Leibniz- Zentrum für Informatik, 2024, 22:1–22:18. url: https://drops.dagstuhl.de/entities/ document/10.4230/LIPIcs.CSL.2024.22

    work page doi:10.4230/lipics.csl.2024.22 2024

  12. [12]

    L. Esakia. Heyting algebras . Ed. by G. Bezhanishvili and W. H. Holliday. Trans. by A. Evseev. Vol. 50. Trends in Logic—Studia Logica Library. English translation of the original 1985 book. Springer, Cham, 2019

    work page 1985

  13. [13]

    Férée et al

    H. Férée et al. ‘Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL’ . In: Automated Reasoning . Springer Nature Switzerland, 2024, pp. 43–60. url: http : //dx.doi.org/10.1007/978-3-031-63501-4_3

    work page doi:10.1007/978-3-031-63501-4_3 2024

  14. [14]

    Fischer-Servi

    G. Fischer-Servi. ‘Axiomatizations for some intuitionistic modal logics’ . In: Rendiconti del Seminario Matematico - PoliTO 42.3 (194), pp. 179–194

    work page

  15. [15]

    J. M. Font. Abstract algebraic logic – An introductory textbook . London: College Publica- tions, 2016

    work page 2016

  16. [16]

    W. Fussner. ‘Interpolation in Non-Classical Logics’ . In: Theory and Applications of Craig Interpolation. Ed. by B. ten Cate et al. Ubiquity Press, 2026

    work page 2026

  17. [17]

    D. M. Gabbay and L. Maksimova. Interpolation and definability: modal and intuitionistic logics. Vol. 1. Oxford University Press, 2005

    work page 2005

  18. [18]

    van der Giessen

    I. van der Giessen. ‘Uniform Interpolation and Admissible Rules: Proof-theoretic invest- igations into (intuitionistic) modal logics’ . PhD thesis. Utrecht University Library. url: http://dx.doi.org/10.33540/1486

    work page doi:10.33540/1486

  19. [19]

    van der Giessen and R

    I. van der Giessen and R. Iemhoff. ‘Sequent Calculi for Intuitionistic Gödel–Löb Logic’ . In: Notre Dame Journal of Formal Logic 62.2 (May 2021). issn: 0029-4527. url: http: //dx.doi.org/10.1215/00294527-2021-0011

    work page doi:10.1215/00294527-2021-0011 2021

  20. [20]

    van der Giessen and I

    I. van der Giessen and I. Shillito. Uniform interpolation with constructive diamond . 2026. url: https://arxiv.org/abs/2602.16880

    work page internal anchor Pith review arXiv 2026

  21. [21]

    On the growth rates of polyregular functions

    M. Girlando et al. ‘Intuitionistic S4 is decidable’ . In: 2023 38th Annual ACM/IEEE Sym- posium on Logic in Computer Science (LICS) . IEEE, June 2023, pp. 1–13. url: http: //dx.doi.org/10.1109/LICS56636.2023.10175684

    work page doi:10.1109/lics56636.2023.10175684 2023

  22. [22]

    P. R. Halmos. ‘Algebraic logic, I. Monadic boolean algebras’ . eng. In: Compositio Math- ematica 12 (1954), pp. 217–249. url: http://eudml.org/doc/88816

    work page 1954

  23. [23]

    R. Iemhoff. ‘Proof Theory for Lax Logic’ . In: Dick de Jongh on Intuitionistic and Provab- ility Logics. Springer International Publishing, 2024, pp. 203–229. url: http://dx.doi. org/10.1007/978-3-031-47921-2_8

    work page doi:10.1007/978-3-031-47921-2_8 2024

  24. [24]

    R. Iemhoff. ‘Uniform interpolation and the existence of sequent calculi’ . In: Annals of Pure and Applied Logic 170.11 (Nov. 2019), p. 102711. issn: 0168-0072. url: http://dx.doi. org/10.1016/j.apal.2019.05.008. 12

    work page doi:10.1016/j.apal.2019.05.008 2019

  25. [25]

    Algebra and Logic16(6), 427–455 (1977)

    L. Maksimova. ‘Craig’s theorem in superintuitionistic logics and amalgamable varieties of pseudo-boolean algebras’ . In: Algebra and Logic 16.6 (Nov. 1977), pp. 427–455. issn: 1573-8302. url: http://dx.doi.org/10.1007/BF01670006

    work page doi:10.1007/bf01670006 1977

  26. [26]

    Maksimova

    L. Maksimova. ‘Interpolation theorems in modal logics and amalgamable varieties of to- pological Boolean algebras’ . In: Algebra and Logic 18.5 (1979), pp. 348–370

    work page 1979

  27. [27]

    M. Marx. ‘Interpolation in Modal Logic’ . In: Algebraic Methodology and Software Techno- logy. Springer Berlin Heidelberg, 1998, pp. 154–163. url: http://dx.doi.org/10.1007/ 3-540-49253-4_13

    work page 1998

  28. [28]

    Marx and C

    M. Marx and C. Areces. ‘Failure of Interpolation in Combined Modal Logics’ . In: Notre Dame Journal of Formal Logic 39.2 (1998), pp. 253–273

    work page 1998

  29. [29]

    Metcalfe

    G. Metcalfe. Interpolation and Amalgamation . 2025. url: https : / / arxiv . org / abs / 2512.00924

    work page arXiv 2025

  30. [30]

    Metcalfe

    G. Metcalfe. ‘Interpolation and Amalgamation’ . In: Theory and Applications of Craig Interpolation. Ed. by B. ten Cate et al. Ubiquity Press, 2026

    work page 2026

  31. [31]

    Muravitsky

    A. Muravitsky. ‘Logic KM: A Biography’ . In: Leo Esakia on Duality in Modal and Intu- itionistic Logics . Springer Netherlands, 2014, pp. 155–185. url: http://dx.doi.org/ 10.1007/978-94-017-8860-1_7

    work page doi:10.1007/978-94-017-8860-1_7 2014

  32. [32]

    de Paiva and S

    V. de Paiva and S. Artemov, eds. Intuitionistic Modal Logic 2017 8 (2021)

    work page 2017

  33. [33]

    Palmigiano

    A. Palmigiano. ‘Dualities for some intuitionistic modal logics’ . In: Liber Amicorum for Dick de Jongh . Institute for Logic, Language and Computation, 2004, pp. 151–167

    work page 2004

  34. [34]

    A. K. Simpson. ‘The Proof Theory and Semantics of Intuitionistic Modal Logic’ . PhD thesis. University of Edinburgh, 1994

    work page 1994

  35. [35]

    Wolter and M

    F. Wolter and M. Zakharyaschev. ‘Intuitionistic Modal Logic’ . In: Logic and Foundations of Mathematics . Springer Netherlands, 1999, pp. 227–238. url: http://dx.doi.org/10. 1007/978-94-017-2109-7_17

    work page 1999

  36. [36]

    Wolter and M

    F. Wolter and M. Zakharyaschev. ‘Intuitionistic Modal Logics as Fragments of Clas- sical Bimodal Logics’ . In: 1997. url: https://api.semanticscholar.org/CorpusID: 6398005. 6 Appendix: Some folklore proofs As noted in the introduction, some results we would expect to be available in the literature from an algebraic and dual theoretic point of view seem to...

    work page 1997