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

TL;DR

This paper introduces a new sequent calculus for intuitionistic Strong L"ob logic that guarantees cut-elimination and strongly terminating proof search, with all proofs formalised in Coq.

Contribution

It presents a novel calculus with syntactic cut-elimination and termination guarantees for intuitionistic Strong L"ob logic, formalised in Coq.

Findings

Syntactic cut-elimination for SL achieved

Backward proof search terminates strongly

Formal proofs verified in Coq

Abstract

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.