Cut-free labelled calculi and decidability for intuitionistic sentential logic with identity

Abstract In this paper we consider the intuitionistic non-Fregean sentential calculus with Suszko’s identity ($\mathsf{ISCI}$). After recalling the basic concepts of the logic and its associated Hilbert proof system, we introduce a new sound and complete class of models for $\mathsf{ISCI}$, called Topological Beth (${\mathsf{TB}}$) models, that can be viewed as algebraic counterparts (and extensions) of sheaf-theoretic topological models of intuitionistic logic. From this semantical study we define a family of sound and cut-free complete labelled calculi that capture both the Kripke and the ${\mathsf{TB}}$ semantics. Using a key property of the forcing relation in ${\mathsf{TB}}$ models, called regularity, we show termination and decidability results. Finally we discuss the automation of the proof search in one of the labelled calculi and its implementation.