Proof Theory for Intuitionistic Strong L\"ob Logic

TL;DR

This paper develops new sequent calculi for intuitionistic strong L"ob logic, proving cut-elimination both syntactically and semantically, and establishing equivalences with Hilbert systems and Kripke models.

Contribution

It introduces two sequent calculi for ${ m iSL}_ox$, proves cut-elimination syntactically and semantically, and links the calculus with Hilbert systems and Kripke models.

Findings

Cut-elimination is proven syntactically for ${ m G3iSL}_ox$.

Semantic proof of completeness using countermodel construction.

Equivalence established between sequent calculi and Hilbert systems.

Abstract

This paper introduces two sequent calculi for intuitionistic strong L\"ob logic ${\sf iSL}_\Box$: a terminating sequent calculus ${\sf G4iSL}_\Box$ based on the terminating sequent calculus ${\sf G4ip}$ for intuitionistic propositional logic ${\sf IPC}$ and an extension ${\sf G3iSL}_\Box$ of the standard cut-free sequent calculus ${\sf G3ip}$ without structural rules for ${\sf IPC}$. One of the main results is a syntactic proof of the cut-elimination theorem for ${\sf G3iSL}_\Box$. In addition, equivalences between the sequent calculi and Hilbert systems for ${\sf iSL}_\Box$ are established. It is known from the literature that ${\sf iSL}_\Box$ is complete with respect to the class of intuitionistic modal Kripke models in which the modal relation is transitive, conversely well-founded and a subset of the intuitionistic relation. Here a constructive proof of this fact is obtained by using a countermodel construction based on a variant of ${\sf G4iSL}_\Box$. The paper thus contains two proofs of cut-elimination, a semantic and a syntactic proof.