TY - GEN
T1 - Sequent calculus in the topos of trees
AU - Clouston, Ranald
AU - Goré, Rajeev
N1 - Publisher Copyright:
© 2015, Springer-Verlag Berlin Heidelberg.
PY - 2015
Y1 - 2015
N2 - Nakano’s “later” modality, inspired by Gödel-Lö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 KMlin. We give a sound and cut-free complete sequent calculus for KMlin 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.
AB - Nakano’s “later” modality, inspired by Gödel-Lö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 KMlin. We give a sound and cut-free complete sequent calculus for KMlin 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.
UR - http://www.scopus.com/inward/record.url?scp=84944060218&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-46678-0_9
DO - 10.1007/978-3-662-46678-0_9
M3 - Conference contribution
SN - 9783662466773
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 133
EP - 147
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
A2 - Pitts, Andrew
PB - Springer Verlag
T2 - 18th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2015 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
Y2 - 11 April 2015 through 18 April 2015
ER -