Copenhagen Programming Language Seminar

A Cut-free Sequent Calculus for Bi-Intuitionistic Logic

Rajeev Goré
Australian National University

Thursday, July 19, Time: 15:15-16:00
DIKU, Universitetsparken 1, Room N034


Bi-intuitionistic logic is the extension of intuitionistic logic with a connective dual to implication. Bi-intuitionistic logic was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent ``cut-free'' sequent calculus for BiInt has recently been shown by Uustalu to fail cut-elimination. We present a new cut-free sequent calculus for BiInt, and prove it sound and complete with respect to its Kripke semantics.
Ensuring completeness is complicated by the interaction between implication and its dual, similarly to future and past modalities in tense logic. Our calculus handles this interaction using sequents which pass information from premises to conclusions using variables instantiated at the leaves of failed derivation trees.
Our simple termination argument allows our calculus to be used for automated deduction.
(Joint work with Linda Buisman.)

Scientific host: Andrzej Filinski. Administrative host: Annette Enggaard. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC. COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body. For more information about COPLAS, see http://www.coplas.org/