Gentzen-Style Sequent Calculus for Semi-intuitionistic Logic

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

STUDIA LOGICA

Kluwer Academic Publishers

Año: 2016

0039-3215

The variety SH of semi-Heyting algebras was introduced by H. P. Sankappanavar(in: Proceedings of the 9th ?Dr. Antonio A. R. Monteiro? Congress, UniversidadNacional 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 semiintuitionistic 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 cuteliminationtheorem for GsH that allows us to prove the decidability of the logic. As adirect consequence, we also obtain the decidability of the equational theory of semi-Heyting algebras.