Relating sequent calculi for Bi-intuitionistic propositional logic

Luís Pinto, Tarmo Uustalu

Research output: Contribution to journalConference articlepeer-review

15 Citations (Scopus)


Bi-intuitionistic logic is the conservative extension of intuitionistic logic with a connective dual to implication. It is sometimes presented as a symmetric constructive subsystem of classical logic. In this paper, we compare three sequent calculi for bi-intuitionistic propositional logic: (1) a basic standard-style sequent calculus that restricts the premises of implication-right and exclusion-left inferences to be single-conclusion resp. single-assumption and is incomplete without the cut rule, (2) the calculus with nested sequents by Goré et al., where a complete class of cuts is encapsulated into special "unnest" rules and (3) a cut-free labelled sequent calculus derived from the Kripke semantics of the logic. We show that these calculi can be translated into each other and discuss the ineliminable cuts of the standard-style sequent calculus.

Original languageEnglish
Pages (from-to)57-72
Number of pages16
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Publication statusPublished - 27 Jan 2011
Event3rd International Workshop on Classical Logic and Computation, CLaC 2010 - Brno, Czech Republic
Duration: 21 Aug 201022 Aug 2010


Dive into the research topics of 'Relating sequent calculi for Bi-intuitionistic propositional logic'. Together they form a unique fingerprint.

Cite this