A New Calculus for Intuitionistic Strong Löb Logic: Strong Termination and Cut-Elimination, Formalised
TABLEAUX 2023, 2023
Best paper award
Abstract
We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong Löb logic, 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.
Recommended citation: Shillito, Ian, van der Giessen, Iris, Goré, Rajeev and Iemhoff, Rosalie. (2023). "A New Calculus for Intuitionistic Strong Löb Logic: Strong Termination and Cut-Elimination, Formalised" TABLEAUX 2023.
Download Paper