pith. sign in

arxiv: 2606.31877 · v1 · pith:QNCDXAWEnew · submitted 2026-06-30 · 💻 cs.LO · cs.CC

Taming Complexity in Intuitionistic Modal Logic: The Case of FIK and Its Shallow Calculus

Han Gao (Institute of Computer Science , Czech Academy of Sciences) , Nicola Olivetti (Aix-Marseille University , CNRS) This is my paper

Pith reviewed 2026-07-01 02:48 UTC · model grok-4.3

classification 💻 cs.LO cs.CC
keywords FIKintuitionistic modal logicshallow sequent calculusnested sequentscut admissibilityEXPSPACEdecision problem
0
0 comments X

The pith

FIK admits a shallow nested sequent calculus that places its decision problem in EXPSPACE.

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

The paper examines FIK, an intuitionistic modal logic positioned strictly between CCDL and IK while using the same bi-relational forcing conditions as IK. It introduces a shallow sequent calculus in which nested sequents are limited to at most one level of nesting. The authors establish syntactic completeness of this calculus by proving admissibility of the cut rule. The restricted nesting depth then yields an EXPSPACE upper bound on the decision problem for FIK, a bound lower than the non-elementary complexity conjectured for IK.

Core claim

FIK possesses a complete shallow sequent calculus consisting of nested sequents with at most one level of nesting; cut is admissible in this calculus, and the resulting decision procedure for FIK lies in EXPSPACE.

What carries the argument

The shallow sequent calculus: nested sequents restricted to at most one level of nesting, which carries both the cut-admissibility proof and the EXPSPACE bound.

If this is right

  • The decision problem for FIK is in EXPSPACE.
  • Cut is admissible in the shallow calculus for FIK.
  • FIK is strictly easier to decide than IK under the conjectured bounds for the latter.
  • The shallow restriction suffices for completeness despite FIK sharing IK's semantics.

Where Pith is reading between the lines

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

  • The complexity gap between FIK and IK may arise precisely from formulas whose proofs in IK demand deeper nesting.
  • The same one-level restriction might be tested on other logics intermediate between CCDL and IK to locate the exact point where EXPSPACE becomes insufficient.
  • An EXPSPACE procedure for FIK could be implemented directly from the shallow calculus and compared against existing solvers for related modal logics.
  • The result separates the semantic strength of the bi-relational models from the syntactic depth needed for proofs.

Load-bearing premise

The shallow calculus is complete for FIK under the same bi-relational forcing conditions used for IK.

What would settle it

A sequent belonging to FIK whose shortest derivation in any complete calculus requires two or more nesting levels, or a counterexample to cut admissibility within the shallow system.

Figures

Figures reproduced from arXiv: 2606.31877 by CNRS), Czech Academy of Sciences), Han Gao (Institute of Computer Science, Nicola Olivetti (Aix-Marseille University.

Figure 1
Figure 1. Figure 1: Forward confluence (left) and backward confluence (right) [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Axiom and rules of C0 CK WK FIK IK [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 4
Figure 4. Figure 4: The calculus SCFIK Definition 3.3 (Size and modal degree of a sequent). Given a sequent Ω = Φ,[Ψ1],...,[Ψl ], its size is defined as |Ω| = |Φ|+|Ψ1|+...+|Ψl |. The size of its output, denoted |Output(Ω)|, is the size of the unique output formula of Ω; the size of its input, denoted |Input(Ω)| is defined as |Ω∗ | Moreover we define md(Ω) = max{md(Φ),md(Ψ1) +1,...,md(Ψl) +1}. The calculus SCFIK for FIK operat… view at source ↗
Figure 5
Figure 5. Figure 5: Examples of proofs in SCFIK Sequents are interpreted according to the location of the output formula and only when the output formula occurs on the top-level the sequents have a formula interpretation. Definition 3.6 (Semantic interpretation). Let M = (W,≤,R,V) be a bi-relational model and x, y ∈ W. For a sequent Ω, we define M, x ⊩ Ω according to the location of its output formula as follows a. if Ω = Φ,[… view at source ↗
Figure 6
Figure 6. Figure 6: SC× FIK, based on quasi-set-sequents Proposition 5.4. Let Φ1 ⊆ Φ2 be two sets of input formulas. The following hold for quasi-set-sequents if ⊢ n SC× FIK Ω,[Φ1],F ◦ then ⊢ n SC× FIK Ω,[Φ1],[Φ2],F ◦ if ⊢ n SC× FIK Ω,[Φ1,F ◦ ] then ⊢ n SC× FIK Ω,[Φ1],[Φ2,F ◦ ] Next, we introduce a more restricted notion of set-sequents called ‘tight sequent’, which is required to generate derivations in which each sequent is… view at source ↗
read the original abstract

Intuitionistic modal logics (IMLs) comprise many systems: from constructive modal logics such as CK and Wijesekera's CCDL to Fischer Servi/Simpson's IK, as well as some recently introduced variants. All of them are characterized by bi-relational semantics and have complete axiomatisations. However, from the perspective of proof theory and complexity, there are strong differences: while for constructive modal logics simple Gentzen calculi suffice, for IK more complex calculi, based on nested or labelled sequents, are needed. As a consequence, the decision problem for constructive modal logics has a PSPACE upper bound, whereas for IK is not known and it is even conjectured to be non-elementary. We study here the proof theory and complexity of FIK, a natural intuitionistic modal logic recently introduced. FIK is strictly in between CCDL and IK, yet it has the same forcing conditions as IK. We define a "shallow" sequent calculus for FIK which is a nested sequent calculus where sequents have at most one level of nesting. We prove its syntactic completeness by showing the admissibility of cut. By means of this calculus we show that decision problem for FIK is in EXPSPACE, whence significantly lower than the complexity conjectured for IK.

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 paper introduces FIK, an intuitionistic modal logic strictly between CCDL and IK that shares the same bi-relational forcing conditions as IK. It defines a shallow nested sequent calculus (nested sequents with at most one level of nesting) for FIK, establishes syntactic completeness by proving cut admissibility, and extracts an EXPSPACE upper bound for the decision problem for FIK from the restricted nesting depth, which is claimed to be significantly lower than the non-elementary complexity conjectured for IK.

Significance. If the shallow calculus is complete for FIK, the result provides a concrete EXPSPACE bound that improves on existing conjectures for related intuitionistic modal logics and demonstrates how restricting nesting depth can tame complexity while preserving completeness via cut admissibility. The syntactic focus and the explicit contrast with IK are strengths that could guide further work on proof systems for this family of logics.

major comments (2)
  1. [Abstract and the section establishing syntactic completeness via cut admissibility] The completeness claim for the shallow calculus (at most one level of nesting) rests on cut admissibility under the bi-relational semantics shared with IK, but the manuscript does not explicitly show that every FIK-valid sequent has a shallow derivation; an additional argument is needed that the nesting restriction does not exclude any theorems, otherwise the EXPSPACE bound applies only to the fragment captured by the calculus rather than to FIK itself.
  2. [The complexity analysis following the cut-admissibility proof] The extraction of the EXPSPACE bound from the one-level nesting structure (as stated in the abstract) presupposes that the calculus is complete; if the completeness step requires deeper nesting for some FIK theorems, the complexity result does not transfer to the full logic.
minor comments (2)
  1. Clarify the precise statement of the bi-relational semantics used for FIK versus IK to make the shared forcing conditions explicit.
  2. Ensure all rule schemas in the shallow calculus are accompanied by side-condition explanations for readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

Thank you for your detailed review and valuable feedback on our manuscript. We appreciate the recognition of the significance of our results on FIK and its shallow calculus. We address each major comment below.

read point-by-point responses

  1. Referee: [Abstract and the section establishing syntactic completeness via cut admissibility] The completeness claim for the shallow calculus (at most one level of nesting) rests on cut admissibility under the bi-relational semantics shared with IK, but the manuscript does not explicitly show that every FIK-valid sequent has a shallow derivation; an additional argument is needed that the nesting restriction does not exclude any theorems, otherwise the EXPSPACE bound applies only to the fragment captured by the calculus rather than to FIK itself.

    Authors: We agree that an explicit demonstration is required to confirm that the shallow calculus is complete for the full FIK, meaning every semantically valid sequent admits a shallow derivation. The cut admissibility establishes equivalence between the cut-free and cut versions of the calculus, but to connect to FIK validity, we will add in the revision a proof that the nesting depth restriction is without loss for FIK. This will be based on the specific modal axioms of FIK allowing us to simulate deeper nestings with shallow ones using the bi-relational models. This addresses the concern and ensures the result applies to FIK. revision: yes

  2. Referee: [The complexity analysis following the cut-admissibility proof] The extraction of the EXPSPACE bound from the one-level nesting structure (as stated in the abstract) presupposes that the calculus is complete; if the completeness step requires deeper nesting for some FIK theorems, the complexity result does not transfer to the full logic.

    Authors: As noted in our response to the first comment, we will provide the missing completeness argument showing that no deeper nesting is required for FIK theorems. Consequently, the EXPSPACE upper bound derived from the one-level nesting will apply to the full logic. We will revise the complexity section to explicitly tie the bound to the now-established completeness of the shallow calculus. revision: yes

Circularity Check

0 steps flagged

No circularity in shallow calculus completeness or EXPSPACE bound for FIK

full rationale

The paper defines a shallow nested sequent calculus (at most one level of nesting), proves syntactic completeness for FIK by cut admissibility under the standard bi-relational semantics, and derives the EXPSPACE upper bound directly from the restricted proof depth. No quoted step reduces a claimed result to a fitted parameter, self-citation, or definitional renaming; the derivation is self-contained via standard syntactic methods without invoking prior author results as load-bearing uniqueness theorems or ansatzes.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claims rest on standard properties of sequent calculi (structural rule admissibility, cut elimination) and the bi-relational semantics shared with IK; no free parameters or new entities are introduced.

axioms (2)
  • domain assumption Cut is admissible in the shallow sequent calculus for FIK
    Invoked to obtain syntactic completeness and then the EXPSPACE bound from bounded nesting depth.
  • standard math Standard structural rules (weakening, contraction) are admissible in nested sequent systems
    Background fact from sequent calculus theory used without re-proof.

pith-pipeline@v0.9.1-grok · 5786 in / 1418 out tokens · 46096 ms · 2026-07-01T02:48:29.604702+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

29 extracted references · 23 canonical work pages

  1. [1]

    In: 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), 288, pp

    Philippe Balbiani, Han Gao, Çi ˘gdem Gencer & Nicola Olivetti (2024): A Natural Intuitionistic Modal Logic: Axiomatization and Bi-Nested Calculus. In: 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), 288, pp. 13:1–13:21, doi:10.4230/LIPIcs.CSL.2024.13

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

  2. [2]

    In: International Joint Conference on Automated Reasoning , Springer, pp

    Philippe Balbiani, Han Gao, Çi ˘gdem Gencer & Nicola Olivetti (2024): Local Intuitionistic Modal Log- ics and Their Calculi . In: International Joint Conference on Automated Reasoning , Springer, pp. 78–96, doi:10.1007/978-3-031-63501-4_5

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

  3. [3]

    Studia Logica, pp

    Philippe Balbiani & Çi ˘gdem Gencer (2026): Intuitionistic Modal Logics: A Minimal Setting. Studia Logica, pp. 1–68, doi:10.1007/s11225-025-10224-7

    work page doi:10.1007/s11225-025-10224-7 2026

  4. [4]

    Logic Journal of the IGPL 34(1), p

    Philippe Balbiani & Çi ˘gdem Gencer (2026): Intuitionistic modal logics: tips and clips. Logic Journal of the IGPL 34(1), p. jzaf089, doi:10.1093/jigpal/jzaf089

    work page doi:10.1093/jigpal/jzaf089 2026

  5. [5]

    In: Proceedings of methods for modalities, 2

    Gianluigi Bellin, Valeria De Paiva & Eike Ritter (2001):Extended Curry-Howard correspondence for a basic constructive modal logic. In: Proceedings of methods for modalities, 2. Available athttps://hdl.handle. net/11562/110

    2001

  6. [6]

    Studia Logica 65(3), pp

    Gavin Bierman & Valeria de Paiva (2000): On an Intuitionistic Modal Logic . Studia Logica 65(3), pp. 383–416, doi:10.1023/A:1005291931660

    work page doi:10.1023/a:1005291931660 2000

  7. [7]

    Kai Brünnler (2009): Deep sequent systems for modal logic . Arch. Math. Log. 48(6), pp. 551–577, doi:10.1007/S00153-009-0137-3

    work page doi:10.1007/s00153-009-0137-3 2009

  8. [8]

    Anupam Das & Sonia Marin (2023): On Intuitionistic Diamonds (and Lack Thereof) . In Revantha Ra- manayake & Josef Urban, editors: Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Lecture Notes in Computer Science 14278, Springer, pp. 283–301, doi:10.1007/978-3-031-43513-3_16

    work page doi:10.1007/978-3-031-43513-3_16 2023

  9. [9]

    Fischer Servi (1977): On modal logic with an intuitionistic base

    Gisèle Fischer Servi (1977): On Modal Logic with an Intuitionistic Base. Studia Logica 36(3), pp. 141–149, doi:10.1007/BF02121259

    work page doi:10.1007/bf02121259 1977

  10. [10]

    Gisèle Fischer Servi (1981): Semantics for a Class of Intuitionistic Modal Calculi , pp. 59–72. Springer Netherlands, Dordrecht, doi:10.1007/978-94-009-8937-5_5

    work page doi:10.1007/978-94-009-8937-5_5 1981

  11. [11]

    Rendiconti del Semi- nario Matematico Università e Politecnico di Torino 42

    Gisèle Fischer Servi (1984): Axiomatizations for some intuitionistic modal logics . Rendiconti del Semi- nario Matematico Università e Politecnico di Torino 42. Available at https://cir.nii.ac.jp/crid/ 1371132818982119684

    1984

  12. [12]

    Fitch (1948): Intuitionistic modal logic with quantifiers

    Frederic B. Fitch (1948): Intuitionistic modal logic with quantifiers. Portugaliae mathematica 7(2), pp. 113–

    1948

  13. [13]

    Available at http://eudml.org/doc/114664

  14. [14]

    169, Springer Science & Business Media, doi:10.1007/978-94-017-2794-5

    Melvin Fitting (2013): Proof methods for modal and intuitionistic logics. 169, Springer Science & Business Media, doi:10.1007/978-94-017-2794-5

    work page doi:10.1007/978-94-017-2794-5 2013

  15. [15]

    Notre Dame J

    Melvin Fitting (2014): Nested Sequents for Intuitionistic Logics . Notre Dame J. Formal Log. 55(1), pp. 41–61, doi:10.1215/00294527-2377869

    work page doi:10.1215/00294527-2377869 2014

  16. [16]

    Journal of Applied Non-Classical Logics 20(4), pp

    Didier Galmiche & Yakoub Salhi (2010): Label-free natural deduction systems for intuitionistic and classical modal logics. Journal of Applied Non-Classical Logics 20(4), pp. 373–421, doi:10.3166/jancl.20.373-421. 426 Taming Complexity in Intuitionistic Modal Logic

    work page doi:10.3166/jancl.20.373-421 2010

  17. [17]

    Journal of Applied Non-Classical Logics , pp

    Han Gao, Marianna Girlando & Nicola Olivetti (2026): A bi-nested calculus for intuitionistic K: proofs and countermodels. Journal of Applied Non-Classical Logics , pp. 1–40, doi:10.1080/11663081.2026.2658653

    work page doi:10.1080/11663081.2026.2658653 2026

  18. [18]

    In: International Workshop on Logic, Language, Information, and Computa- tion, Springer, pp

    Marianna Girlando, Roman Kuznets, Sonia Marin, Marianela Morales & Lutz Straßburger (2024): A simple loopcheck for intuitionistic K. In: International Workshop on Logic, Language, Information, and Computa- tion, Springer, pp. 47–63, doi:10.1007/978-3-031-62687-6_4

    work page doi:10.1007/978-3-031-62687-6_4 2024

  19. [19]

    Logical Methods in Computer Science V olume 7, Issue 2:8, doi:10.2168/LMCS-7(2:8)2011

    Rajeev Goré, Linda Postniece & Alwen F Tiu (2011): On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics . Logical Methods in Computer Science V olume 7, Issue 2:8, doi:10.2168/LMCS-7(2:8)2011

    work page doi:10.2168/lmcs-7(2:8)2011 2011

  20. [20]

    de Groot, I

    Jim de Groot, Ian Shillito & Ranald Clouston (2025): Semantical analysis of intuitionistic modal logics between CK and IK. In: 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , IEEE, pp. 169–182, doi:10.1109/LICS65433.2025.00020

    work page doi:10.1109/lics65433.2025.00020 2025

  21. [21]

    Archive for Mathematical Logic 58(3), pp

    Roman Kuznets & Lutz Straßburger (2019): Maehara-style modal nested calculi. Archive for Mathematical Logic 58(3), pp. 359–385, doi:10.1007/s00153-018-0636-1

    work page doi:10.1007/s00153-018-0636-1 2019

  22. [22]

    Sonia Marin, Marianela Morales & Lutz Straßburger (2021): A fully labelled proof system for intuitionistic modal logics. J. Log. Comput. 31(3), pp. 998–1022, doi:10.1093/LOGCOM/EXAB020

    work page doi:10.1093/logcom/exab020 2021

  23. [23]

    Context Representation and Reasoning (CRR-2005) 13

    Michael Mendler & Valeria de Paiva (2005): Constructive CK for contexts . Context Representation and Reasoning (CRR-2005) 13. Available at https://ceur-ws.org/Vol-136/143.pdf

    2005

  24. [24]

    Odintsov & Heinrich Wansing (2008): Inconsistency-tolerant description logic

    Sergei P. Odintsov & Heinrich Wansing (2008): Inconsistency-tolerant description logic. Part II: A tableau algorithm for CALCC. Journal of Applied Logic 6(3), pp. 343–360, doi:10.1016/j.jal.2007.06.001

    work page doi:10.1016/j.jal.2007.06.001 2008

  25. [25]

    In: Proceed- ings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge (TARK) , pp

    Gordon Plotkin & Colin Stirling (1986): A framework for intuitionistic modal logics . In: Proceed- ings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge (TARK) , pp. 399–406, doi:10.5555/1029786.1029823

    work page doi:10.5555/1029786.1029823 1986

  26. [26]

    Dover Publications, Mineola, N.Y ., doi:10.2307/2271676

    Dag Prawitz (1965): Natural Deduction: A Proof-Theoretical Study . Dover Publications, Mineola, N.Y ., doi:10.2307/2271676

    work page doi:10.2307/2271676 1965

  27. [27]

    Alex K Simpson (1994): The proof theory and semantics of intuitionistic modal logic . Ph.D. thesis, School of College of Science and Engineering, University of Edinburgh. Available at http://hdl.handle.net/ 1842/407

    1994

  28. [28]

    Lutz Straßburger (2013): Cut elimination in nested sequents for intuitionistic modal logics. In: Foundations of Software Science and Computation Structures: 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings 16 , Springer, p...

    work page doi:10.1007/978-3-642-37075-5_14 2013

  29. [29]

    Duminda Wijesekera (1990): Constructive Modal Logics I . Ann. Pure Appl. Log. 50(3), pp. 271–301, doi:10.1016/0168-0072(90)90059-B

    work page doi:10.1016/0168-0072(90)90059-b 1990