pith. sign in

arxiv: 2511.04577 · v2 · pith:AQMMZ5UUnew · submitted 2025-11-06 · 💻 cs.LO

The Size of Interpolants in Modal Logics

Balder ten Cate , Louwe Kuijer , Frank Wolter This is my paper

Pith reviewed 2026-05-17 23:41 UTC · model grok-4.3

classification 💻 cs.LO
keywords modal logicCraig interpolationuniform interpolationstrongest implicatestabular logicsinterpolant sizenormal modal logicsS4
0
0 comments X

The pith

Tabular modal logics reduce strongest implicates to polynomial-sized propositional interpolants, while non-tabular logics require exponential size.

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

The paper examines the size of Craig interpolants, uniform interpolants, and strongest implicates across modal logics. It proves that tabular logics, those with only finitely many non-equivalent formulas of any given modal depth, admit a polynomial-time reduction from strongest implicate computation to uniform interpolant computation in classical propositional logic. As a direct result, these implicates have polynomial DAG size if and only if NP is contained in P/poly. The reduction carries over to Craig and uniform interpolants whenever the tabular logic satisfies the Craig interpolation property. For almost all non-tabular standard normal modal logics an unconditional exponential lower bound on interpolant size holds, producing a clean dichotomy for any normal modal logic contained in or containing S4 or GL.

Core claim

For tabular modal logics, the computation of strongest implicates can be reduced in polynomial time to uniform interpolant computation in classical propositional logic. Hence they are of polynomial dag-size iff NP is included in P/poly. The reduction also holds for Craig interpolants and uniform interpolants if the tabular modal logic has the Craig interpolation property. For normal modal logics contained in or containing S4 or GL we obtain the following dichotomy: tabular logics have propositionally sized interpolants while for non-tabular logics an unconditional exponential lower bound holds.

What carries the argument

Tabularity of the modal logic (finitely many non-equivalent formulas per modal depth), which permits the polynomial-time reduction of modal strongest implicates to classical propositional uniform interpolants.

If this is right

  • Strongest implicates in any tabular modal logic have polynomial DAG size precisely when NP is contained in P/poly.
  • In tabular modal logics that possess the Craig interpolation property, both Craig interpolants and uniform interpolants inherit the same polynomial-size characterization.
  • Almost all non-tabular standard normal modal logics have an unconditional exponential lower bound on the size of their Craig interpolants and strongest implicates.
  • Any normal modal logic contained in or containing S4 or GL obeys a strict size dichotomy: polynomial when tabular, exponential when non-tabular.

Where Pith is reading between the lines

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

  • The tabularity distinction may serve as a general classifier for interpolant complexity across wider families of modal logics beyond those containing or contained in S4 or GL.
  • Practical modal logics that turn out to be tabular could support efficient interpolant-based algorithms in verification or knowledge-base tasks.
  • The reduction technique might be adapted to obtain size bounds for related notions such as Beth definability in the same tabular setting.

Load-bearing premise

The logic must be tabular to obtain the polynomial upper bound via reduction and non-tabular to obtain the unconditional exponential lower bound.

What would settle it

An explicit non-tabular normal modal logic for which some Craig interpolant or strongest implicate has only polynomial DAG size would refute the exponential lower bound.

read the original abstract

We start a systematic investigation of the size of Craig interpolants, uniform interpolants, and strongest implicates for (quasi-)normal modal logics. Our main upper bound states that for tabular modal logics, the computation of strongest implicates can be reduced in polynomial time to uniform interpolant computation in classical propositional logic. Hence they are of polynomial dag-size iff NP is included in P/poly. The reduction also holds for Craig interpolants and uniform interpolants if the tabular modal logic has the Craig interpolation property. Our main lower bound shows an unconditional exponential lower bound on the size of Craig interpolants and strongest implicates covering almost all non-tabular standard normal modal logics. For normal modal logics contained in or containing S4 or GL we obtain the following dichotomy: tabular logics have ``propositionally sized'' interpolants while for non-tabular logics an unconditional exponential lower bound holds.

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

1 major / 0 minor

Summary. The paper claims that for tabular modal logics, the computation of strongest implicates reduces in polynomial time to uniform interpolant computation in classical propositional logic, implying they have polynomial DAG-size if and only if NP is included in P/poly. The reduction extends to Craig interpolants and uniform interpolants when the logic has the Craig interpolation property. For almost all non-tabular standard normal modal logics, the paper establishes unconditional exponential lower bounds on the size of Craig interpolants and strongest implicates. For normal modal logics contained in or containing S4 or GL, this yields a dichotomy: tabular logics admit propositionally sized interpolants while non-tabular ones have unconditional exponential lower bounds.

Significance. If the central reductions and bounds hold, the results deliver a clean complexity-theoretic classification of interpolant sizes across tabular and non-tabular modal logics, directly tying modal interpolation to the propositional case and the P/poly question. The unconditional exponential lower bounds for non-tabular logics and the resulting dichotomy for logics around S4 and GL constitute a substantial advance, providing falsifiable predictions that distinguish broad classes of modal logics by interpolant size.

major comments (1)
  1. [Reduction for tabular logics (likely §4 or the main technical section establishing the upper bound)] The central upper-bound claim (abstract and the reduction for tabular logics) asserts a polynomial-time reduction from strongest-implicate computation to propositional uniform interpolation. However, tabularity only guarantees finitely many non-equivalent formulas per modal depth; this finite number is typically exponential (or worse) in the depth. The manuscript must specify the exact encoding used in the reduction and demonstrate that it can be constructed in polynomial time without explicit enumeration of equivalence classes, as any such enumeration would produce an exponential-size propositional instance and undermine both the polynomial-time claim and the subsequent complexity equivalence.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful and constructive report. The comment on the reduction for tabular logics raises an important point about clarity in the presentation of the polynomial-time claim. We address it below and will revise the manuscript accordingly.

read point-by-point responses

  1. Referee: The central upper-bound claim (abstract and the reduction for tabular logics) asserts a polynomial-time reduction from strongest-implicate computation to propositional uniform interpolation. However, tabularity only guarantees finitely many non-equivalent formulas per modal depth; this finite number is typically exponential (or worse) in the depth. The manuscript must specify the exact encoding used in the reduction and demonstrate that it can be constructed in polynomial time without explicit enumeration of equivalence classes, as any such enumeration would produce an exponential-size propositional instance and undermine both the polynomial-time claim and the subsequent complexity equivalence.

    Authors: We agree that the current presentation of the reduction in Section 4 could be clearer on this point. The reduction does not enumerate equivalence classes explicitly. Instead, it constructs a propositional formula whose variables are in one-to-one correspondence with the subformulas of the input modal formula (together with the propositional atoms), and tabularity is used only to guarantee that the uniform interpolant in the resulting propositional instance correctly captures the strongest implicate. Because the construction follows the syntax tree of the input formula, its size and running time remain polynomial in the size of the input; no enumeration of the (potentially exponential) set of types is performed. We will add a detailed description of this encoding together with a formal argument that the reduction avoids explicit enumeration, thereby preserving the polynomial-time bound and the complexity-theoretic equivalence. revision: yes

Circularity Check

0 steps flagged

No circularity: upper and lower bounds derived from independent reductions and frame arguments

full rationale

The paper establishes its main results through explicit polynomial-time reductions from strongest-implicate computation in tabular modal logics to uniform interpolant computation in propositional logic, plus direct exponential lower-bound arguments on non-tabular frames. These steps rely on the standard definition of tabular logics (finitely many inequivalent formulas per modal depth) and the Craig interpolation property when invoked, without any self-definitional equations, fitted parameters renamed as predictions, or load-bearing self-citations whose justification collapses back into the current paper. The derivation chain is therefore self-contained and externally verifiable against existing modal-logic complexity results.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The results rest on the standard definitions and semantics of normal modal logics together with the classical notions of Craig interpolation, uniform interpolation, and strongest implicates; no new entities or fitted parameters are introduced.

axioms (1)
  • standard math Standard Kripke semantics and axioms for normal modal logics (including S4 and GL).
    Invoked to define tabular vs. non-tabular logics and to establish the interpolation properties used in the reductions.

pith-pipeline@v0.9.0 · 5445 in / 1376 out tokens · 39092 ms · 2026-05-17T23:41:14.677531+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

37 extracted references · 37 canonical work pages

  1. [1]

    Noga Alon and Ravi B. Boppana. The monotone circuit complexity of boolean functions. Comb. , 7(1):1--22, 1987. https://doi.org/10.1007/BF02579196 doi:10.1007/BF02579196

    work page doi:10.1007/bf02579196 1987

  2. [2]

    Computational Complexity - A Modern Approach

    Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach . Cambridge University Press, 2009. URL: http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521424264

    work page 2009

  3. [3]

    Living without beth and craig: Definitions and interpolants in description and modal logics with nominals and role inclusions,

    Alessandro Artale, Jean Christoph Jung, Andrea Mazzullo, Ana Ozaki, and Frank Wolter. Living without B eth and C raig: Definitions and interpolants in description and modal logics with nominals and role inclusions. ACM Trans. Comput. Log. , 24(4):34:1--34:51, 2023. https://doi.org/10.1145/3597301 doi:10.1145/3597301

    work page doi:10.1145/3597301 2023

  4. [4]

    Uniform interpolation and propositional quantifiers in modal logics

    Marta B \' lkov \' a . Uniform interpolation and propositional quantifiers in modal logics. Stud Logica , 85(1):1--31, 2007. URL: https://doi.org/10.1007/s11225-007-9021-5, https://doi.org/10.1007/S11225-007-9021-5 doi:10.1007/S11225-007-9021-5

    work page doi:10.1007/s11225-007-9021-5 2007

  5. [5]

    Modal Logic

    Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic . Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001

    work page 2001

  6. [6]

    Chagrov and Michael Zakharyaschev

    Alexander V. Chagrov and Michael Zakharyaschev. Modal Logic , volume 35 of Oxford logic guides . Oxford University Press, 1997

    work page 1997

  7. [7]

    Logical questions concerning the mu-calculus: Interpolation, lyndon and los-tarski

    Giovanna D'Agostino and Marco Hollenberg. Logical questions concerning the mu-calculus: Interpolation, lyndon and los-tarski. J. Symb. Log. , 65(1):310--332, 2000. https://doi.org/10.2307/2586539 doi:10.2307/2586539

    work page doi:10.2307/2586539 2000

  8. [8]

    Mechanised uniform interpolation for modal logics k, gl, and isl

    Hugo F \' e r \' e e, Iris van der Giessen, Sam van Gool, and Ian Shillito. Mechanised uniform interpolation for modal logics k, gl, and isl. In Christoph Benzm \" u ller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II , volume 1...

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

  9. [9]

    Craig's interpolation theorem for modal logics

    Dov M Gabbay. Craig's interpolation theorem for modal logics. In Conference in mathematical logic—London’70 , pages 111--127. Springer, 1972

    work page 1972

  10. [10]

    Gabbay and Larisa Maksimova

    Dov M. Gabbay and Larisa Maksimova. Interpolation and Definability: Modal and Intuitionistic Logics . Oxford University Press, 2005

    work page 2005

  11. [11]

    Oxford Univer- sity Press (2018).https://doi.org/10.1093/oso/9780198814788.001.0001

    Dov M. Gabbay and Larisa Maksimova. Interpolation and Definability: Modal and Intuitionistic Logics . Oxford University Press, 05 2005. https://doi.org/10.1093/acprof:oso/9780198511748.001.0001 doi:10.1093/acprof:oso/9780198511748.001.0001

    work page doi:10.1093/acprof:oso/9780198511748.001.0001 2005

  12. [12]

    Advances in Modal Logic,

    Silvio Ghilardi, Carsten Lutz, Frank Wolter, and Michael Zakharyaschev. Conservative extensions in modal logic. In Guido Governatori, Ian M. Hodkinson, and Yde Venema, editors, Advances in Modal Logic 6, papers from the sixth conference on "Advances in Modal Logic," held in Noosa, Queensland, Australia, on 25-28 September 2006 , pages 187--207. College Pu...

    work page 2006

  13. [13]

    Zawadowski

    Silvio Ghilardi and Marek W. Zawadowski. Undefinability of propositional quantifiers in the modal system S4 . Stud Logica , 55(2):259--271, 1995

    work page 1995

  14. [14]

    Modal separation of fixpoint formulae

    Jean Christoph Jung and Jedrzej Kolodziejski. Modal separation of fixpoint formulae. In Olaf Beyersdorff, Michal Pilipczuk, Elaine Pimentel, and Kim Thang Nguyen, editors, 42nd International Symposium on Theoretical Aspects of Computer Science, STACS 2025, March 4-7, 2025, Jena, Germany , volume 327 of LIPIcs , pages 55:1--55:20. Schloss Dagstuhl - Leibni...

    work page doi:10.4230/lipics.stacs.2025.55 2025

  15. [15]

    Computation of interpolants for description logic concepts in hard cases

    Jean Christoph Jung, J e drzej Ko odziejski, and Frank Wolter. Computation of interpolants for description logic concepts in hard cases. arXiv preprint arXiv:2507.15689 , 2025

    work page arXiv 2025

  16. [16]

    Separating data examples by description logic concepts with restricted signatures

    Jean Christoph Jung, Carsten Lutz, Hadrien Pulcini, and Frank Wolter. Separating data examples by description logic concepts with restricted signatures. In Meghyn Bienvenu, Gerhard Lakemeyer, and Esra Erdem, editors, Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, KR 2021, Online event, November 3-...

    work page doi:10.24963/kr.2021/37 2021

  17. [17]

    In: 2021 36th Annual ACM/IEEE Sym- posium on Logic in Computer Science (LICS)

    Jean Christoph Jung and Frank Wolter. Living without beth and craig: Definitions and interpolants in the guarded and two-variable fragments. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021 , pages 1--14. IEEE , 2021. https://doi.org/10.1109/LICS52264.2021.9470585 doi:10.1109/LICS52264.2021.9470585

    work page doi:10.1109/lics52264.2021.9470585 2021

  18. [18]

    Turing machines that take advice

    Richard Karp. Turing machines that take advice. Enseign. Math. , 28:191--209, 1982

    work page 1982

  19. [19]

    Some connections between nonuniform and uniform complexity classes

    Richard M Karp and Richard J Lipton. Some connections between nonuniform and uniform complexity classes. In Proceedings of the twelfth annual ACM symposium on Theory of computing , pages 302--309, 1980

    work page 1980

  20. [20]

    Interpolation in classical propositional logic, 2025

    Patrick Koopmann, Christoph Wernhard, and Frank Wolter. Interpolation in classical propositional logic, 2025. URL: https://arxiv.org/abs/2508.11449, https://arxiv.org/abs/2508.11449 arXiv:2508.11449

    work page arXiv 2025

  21. [21]

    Tools and Techniques in Modal Logic

    Marcus Kracht. Tools and Techniques in Modal Logic . Elsevier, 1999

    work page 1999

  22. [22]

    A non-uniform view of C raig interpolation in modal logics with linear frames

    Agi Kurucz, Frank Wolter, and Michael Zakharyaschev. A non-uniform view of C raig interpolation in modal logics with linear frames. CoRR , abs/2312.05929, 2023

    work page arXiv 2023

  23. [23]

    The ghosts of forgotten things: A study on size after forgetting

    Paolo Liberatore. The ghosts of forgotten things: A study on size after forgetting. Ann. Pure Appl. Log. , 175(8):103456, 2024. URL: https://doi.org/10.1016/j.apal.2024.103456, https://doi.org/10.1016/J.APAL.2024.103456 doi:10.1016/J.APAL.2024.103456

    work page doi:10.1016/j.apal.2024.103456 2024

  24. [24]

    In: Walsh, T

    Carsten Lutz and Frank Wolter. Foundations for uniform interpolation and forgetting in expressive description logics. In IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011 , pages 989--995. IJCAI/AAAI , 2011. https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-170 doi:...

    work page doi:10.5591/978-1-57735-516-8/ijcai11-170 2011

  25. [25]

    Interpolation in modal logic

    Maarten Marx. Interpolation in modal logic. In Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology, AMAST 1998 , pages 154--163. Springer, 1998

    work page 1998

  26. [26]

    A lower bound for the complexity of C raig's interpolants in sentential logic

    Daniele Mundici. A lower bound for the complexity of C raig's interpolants in sentential logic. Arch. Math. Log. , 23(1):27--36, 1983. https://doi.org/10.1007/BF02023010 doi:10.1007/BF02023010

    work page doi:10.1007/bf02023010 1983

  27. [27]

    Exponential lower bounds on definable fixed points

    Konstantinos Papafilippou and David Fern \' a ndez - Duque. Exponential lower bounds on definable fixed points. In J \" o rg Endrullis and Sylvain Schmitz, editors, 33rd EACSL Annual Conference on Computer Science Logic, CSL 2025, February 10-14, 2025, Amsterdam, Netherlands , volume 326 of LIPIcs , pages 25:1--25:19. Schloss Dagstuhl - Leibniz-Zentrum f ...

    work page doi:10.4230/lipics.csl.2025.25 2025

  28. [28]

    Andrew M. Pitts. On an interpretation of second order quantification in first order intuitionistic propositional logic. J. Symb. Log. , 57(1):33--52, 1992. https://doi.org/10.2307/2275175 doi:10.2307/2275175

    work page doi:10.2307/2275175 1992

  29. [29]

    Lower bounds on the monotone complexity of some boolean functions

    Alexander Alexandrovich Razborov. Lower bounds on the monotone complexity of some boolean functions. In Doklady Akademii Nauk , volume 281, pages 798--801. Russian Academy of Sciences, 1985

    work page 1985

  30. [30]

    Formulas versus circuits for small distance connectivity

    Benjamin Rossman. Formulas versus circuits for small distance connectivity. SIAM J. Comput. , 47(5):1986--2028, 2018. https://doi.org/10.1137/15M1027310 doi:10.1137/15M1027310

    work page doi:10.1137/15m1027310 1986

  31. [31]

    A note on the size of C raig interpolants

    Uwe Sch \" o ning and Jacobo Tor \' a n. A note on the size of C raig interpolants. In Thomas Schwentick, Denis Th \' e rien, and Heribert Vollmer, editors, Circuits, Logic, and Games, 08.11. - 10.11.2006 , volume 06451 of Dagstuhl Seminar Proceedings . Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 20...

    work page 2006

  32. [32]

    Uniform interpolation in coalgebraic modal logic

    Fatemeh Seifan, Lutz Schr \" o der, and Dirk Pattinson. Uniform interpolation in coalgebraic modal logic. CoRR , abs/2205.00448, 2022. URL: https://doi.org/10.48550/arXiv.2205.00448, https://arxiv.org/abs/2205.00448 arXiv:2205.00448 , https://doi.org/10.48550/ARXIV.2205.00448 doi:10.48550/ARXIV.2205.00448

    work page doi:10.48550/arxiv.2205.00448 2022

  33. [33]

    Definitorially complete description logics

    Balder ten Cate, Willem Conradie, Maarten Marx, and Yde Venema. Definitorially complete description logics. In Proc.\ of KR , pages 79--89, 2006

    work page 2006

  34. [34]

    Beth definability in expressive description logics

    Balder ten Cate, Enrico Franconi, and Inan c Seylan. Beth definability in expressive description logics. J. Artif. Intell. Res. , 48:347--414, 2013

    work page 2013

  35. [35]

    Uniform interpolation via nested sequents and hypersequents

    Iris van der Giessen, Raheleh Jalali, and Roman Kuznets. Uniform interpolation via nested sequents and hypersequents. J. Log. Comput. , 35(6), 2025. URL: https://doi.org/10.1093/logcom/exae053, https://doi.org/10.1093/LOGCOM/EXAE053 doi:10.1093/LOGCOM/EXAE053

    work page doi:10.1093/logcom/exae053 2025

  36. [36]

    o del'96: Logical foundations of mathematics, computer science and physics---Kurt G \

    Albert Visser et al. Uniform interpolation and layered bisimulation. In G \"o del'96: Logical foundations of mathematics, computer science and physics---Kurt G \"o del's legacy , pages 139--164. Association for Symbolic Logic, 1996

    work page 1996

  37. [37]

    Modal decision problems

    Frank Wolter and Michael Zakharyaschev. Modal decision problems. In Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors, Handbook of Modal Logic , volume 3 of Studies in logic and practical reasoning , pages 427--489. North-Holland, 2007. URL: https://doi.org/10.1016/s1570-2464(07)80010-3, https://doi.org/10.1016/S1570-2464(07)80010-3 do...

    work page doi:10.1016/s1570-2464(07)80010-3 2007