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