A Cut-free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version
Linda Buisman, Rajeev Gor\'e

TL;DR
This paper introduces a new cut-free sequent calculus for bi-intuitionistic logic, overcoming previous limitations by handling implication duality with extended sequents, and proves its soundness and completeness.
Contribution
It presents the first sound and complete cut-free sequent calculus for bi-intuitionistic logic that manages implication duality through extended sequents.
Findings
The calculus is sound and complete with respect to Kripke semantics.
It enables automated deduction due to its termination properties.
Handles interaction between implication and its dual effectively.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Logic, programming, and type systems · Semantic Web and Ontologies
