Gentzen-Style Sequent Calculus for Semi-intuitionistic Logic

Abstract

The variety SH of semi-Heyting algebras was introduced by H. P. Sankappanavar (in: Proceedings of the 9th “Dr. Antonio A. R. Monteiro” Congress, Universidad Nacional del Sur, Bahía Blanca, 2008) [13] as an abstraction of the variety of Heyting algebras. Semi-Heyting algebras are the algebraic models for a logic HsH, known as semi-intuitionistic logic, which is equivalent to the one defined by a Hilbert style calculus in Cornejo (Studia Logica 98(1–2):9–25, 2011) [6]. In this article we introduce a Gentzen style sequent calculus GsH for the semi-intuitionistic logic whose associated logic GsH is the same as HsH. The advantage of this presentation of the logic is that we can prove a cut-elimination theorem for GsH 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.