A cut-free sequent calculus for bi-intuitionistic logic
Date
2007
Authors
Postniece (previously Buisman), Linda
Gore, Rajeev
Journal Title
Journal ISSN
Volume Title
Publisher
Springer
Abstract
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 extended 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, although this is not its main purpose.
Description
Keywords
Keywords: Boolean algebra; Codes (symbols); Information systems; Message passing; Semantics; Bi-intuitionistic logic; Cut-free sequent calculus; Termination argument; Logic programming
Citation
Collections
Source
Proceedings of TABLEAUX 2007
Type
Conference paper
Book Title
Entity type
Access Statement
License Rights
DOI
Restricted until
2037-12-31