A new calculus for intuitionistic Strong L\'ob logic: strong termination and cut-elimination, formalised

Autor:	Shillito, Ian, van der Giessen, Iris, Goré, Rajeev, Iemhoff, Rosalie
Rok vydání:	2023
Předmět:	Computer Science - Logic in Computer Science Mathematics - Logic F.4.1
Druh dokumentu:	Working Paper
Popis:	We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong L\"ob logic $\sf{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. Comment: 21-page conference paper + 4-page appendix with proofs
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2309.00486 Zobrazit plný text záznamu View this record from Arxiv