Sequent Calculus in the Topos of Trees

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 $\mathrm{KM}_{\mathrm{lin}}$. We give a sound and cut-free complete sequent calculus for $\mathrm{KM}_{\mathrm{lin}}$ 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 decision procedure can be restricted to drop linearity and hence capture KM.