We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong Löb logic $$\textsf{iSL}$$, an intuitionistic modal logic with a provability interpretation. A novel measure on sequents is used to prove both the termination of the naive backward proof search strategy, and the admissibility of cut in a syntactic and direct way, leading to a straightforward cut-elimination procedure. All proofs have been formalised in the interactive theorem prover Coq.
CITATION STYLE
Shillito, I., van der Giessen, I., Goré, R., & Iemhoff, R. (2023). A New Calculus for Intuitionistic Strong Löb Logic: Strong Termination and Cut-Elimination, Formalised. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 14278 LNAI, pp. 73–93). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-43513-3_5
Mendeley helps you to discover research relevant for your work.