A cut-free sequent calculus for bi-intuitionistic logic
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...[Show more]
|Collections||ANU Research Publications|
|Source:||Proceedings of TABLEAUX 2007|
|01_Postniece (previously Buisman)_A_cut-free_sequent_calculus_2007.pdf||451.67 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.