Gentzen-Style Sequent Calculus for Semi-intuitionistic Logic

Studia Logica 104 (6):1245-1265 (2016)
  Copy   BIBTEX


The variety \ of semi-Heyting algebras was introduced by H. P. Sankappanavar [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 :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.



    Upload a copy of this work     Papers currently archived: 92,283

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

The Semi Heyting–Brouwer Logic.Juan Manuel Cornejo - 2015 - Studia Logica 103 (4):853-875.
Semi-intuitionistic Logic.Juan Manuel Cornejo - 2011 - Studia Logica 98 (1-2):9-25.
An algebraic approach to intuitionistic connectives.Xavier Caicedo & Roberto Cignoli - 2001 - Journal of Symbolic Logic 66 (4):1620-1636.
n‐linear weakly Heyting algebras.Sergio A. Celani - 2006 - Mathematical Logic Quarterly 52 (4):404-416.
Unification in intuitionistic logic.Silvio Ghilardi - 1999 - Journal of Symbolic Logic 64 (2):859-880.


Added to PP

16 (#911,480)

6 months
2 (#1,206,195)

Historical graph of downloads
How can I increase my downloads?