Relating Sequent Calculi for Bi-intuitionistic Propositional Logic

Details Relating Sequent Calculi for Bi-intuitionistic Propositional Logic Relating Sequent Calculi for Bi-intuitionistic Propositional Logic

2011-01-28

arxiv.org/abs/1101.5445v1

EPTCS 47, 2011, pp. 57-72

Computer Science

Logic in Computer Science

In Proceedings CL&C 2010, arXiv:1101.5200

Scientific paper

10.4204/EPTCS.47.7

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 Gore 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.

Affiliated with

Also associated with

No associations

Rating

Relating Sequent Calculi for Bi-intuitionistic Propositional Logic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Relating Sequent Calculi for Bi-intuitionistic Propositional Logic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Relating Sequent Calculi for Bi-intuitionistic Propositional Logic will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-551460