Sequent Calculus in the Topos of Trees
Ranald Clouston, Rajeev Gor\'e

TL;DR
This paper introduces a new sequent calculus for a propositional modal logic combining intuitionistic and linear features, providing a decision procedure with proven decidability and complexity results.
Contribution
It presents a sound, complete, and cut-free sequent calculus for the logic KM_lin, enabling deterministic proof search and decidability analysis.
Findings
The calculus is sound, complete, and cut-free.
Proof search terminates and is deterministic.
The validity problem is coNP-complete.
Abstract
Nakano's "later" modality, inspired by G\"{o}del-L\"{o}b provability logic, has been applied in type systems and program logics to capture guarded recursion. Birkedal et al modelled this modality via the internal logic of the topos of trees. We show that the semantics of the propositional fragment of this logic can be given by linear converse-well-founded intuitionistic Kripke frames, so this logic is a marriage of the intuitionistic modal logic KM and the intermediate logic LC. We therefore call this logic . We give a sound and cut-free complete sequent calculus for via a strategy that decomposes implication into its static and irreflexive components. Our calculus provides deterministic and terminating backward proof-search, yields decidability of the logic and the coNP-completeness of its validity problem. Our calculus and…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Formal Methods in Verification
