Postniece (previously Buisman), Linda; Gore, Rajeev
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]
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.