Gentzen-style sequent calculus for semi-intuitionistic logic

CORNEJO, JUAN MANUEL; CASTAÑO, DIEGO NICOLÁS

STUDIA LOGICA

Springer Netherlands

Año: 2016 p. 1 - 21

0039-3215

The variety $mathcal{SH}$ of semi-Heyting algebras was introduced by H. P. Sankappanavar in cite{sankappanavar2008semi} as an abstraction of the variety of Heyting algebras. Semi-Heyting algebras are the algebraic models for a logic $SI$, known as {it semi-intuitionistic logic}, which is equivalent to the one defined by a Hilbert style calculus in cite{cornejo2011semi}. In this article we introduce a Gentzen style sequent calculus $LSJ$ for the semi-intuitionistic logic whose associated logic $LSJ$ is the same as $SI$. The advantage of this presentation of the logic is that we can prove a cut-elimination theorem for $LSJ$ that allows us to prove the decidability of the logic. As a direct consequence, we also obtain the decidability of the equational theory of semi-Heyting algebras.