## Relating sequent calculi for bi-intuitionistic propositional logic

Institute of Cybernetics

Thursday, 9 September 2010, 14:00

Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

**Abstract**: 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.

I will 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.

I will show that these calculi can be translated into each other
and discuss the ineliminable cuts of the standard-style sequent
calculus.

(Joint work with Luís Pinto.)

Tarmo Uustalu

Last update 10 September 2010