Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents
In Carlos Areces & Robert Goldblatt (eds.), Advances in Modal Logic, Volume 7. CSLI Publications. pp. 43-66 (2008)
Abstract
We propose a new sequent calculus for bi intuitionistic logic which sits somewhere between display calculi and traditional sequent calculi by using nested sequents. Our calculus enjoys a simple (purely syntactic) cut elimination proof as do display calculi. But it has an easily derivable variant calculus which is amenable to automated proof search as are (some) traditional sequent calculi. We first present the initial calculus and its cut elimination proof. We then present the derived calculus, and then present a proof search strategy which allows it to be used for automated proof search. We prove that this search strategy is terminating and complete by showing how it can be used to mimic derivations obtained from an existing calculus GBiInt for bi intuitionistic logic. As far as we know, our new calculus is the first sequent calculus for bi intuitionistic logic which uses no semantic additions like labels, which has a purely syntactic cut elimination proof, and which can be used naturally for backwards proof search. Keywords: Bi-intuitionistic logic, display calculi, proof search.My notes
Similar books and articles
Cut-elimination and a permutation-free sequent calculus for intuitionistic logic.Roy Dyckhoff & Luis Pinto - 1998 - Studia Logica 60 (1):107-118.
Admissibility of structural rules for contraction-free systems of intuitionistic logic.Roy Dyckhoff & Sara Negri - 2000 - Journal of Symbolic Logic 65 (4):1499-1518.
Effective Cut-elimination for a Fragment of Modal mu-calculus.Grigori Mints - 2012 - Studia Logica 100 (1-2):279-287.
A Simple Proof of Completeness and Cut-elimination for Propositional G¨ odel Logic.Arnon Avron - unknown
Indexed systems of sequents and cut-elimination.Grigori Mints - 1997 - Journal of Philosophical Logic 26 (6):671-696.
Analytics
Added to PP
2009-01-28
Downloads
42 (#279,985)
6 months
1 (#448,551)
2009-01-28
Downloads
42 (#279,985)
6 months
1 (#448,551)
Historical graph of downloads
Citations of this work
Constructive negation, implication, and co-implication.Heinrich Wansing - 2008 - Journal of Applied Non-Classical Logics 18 (2-3):341-364.
Natural deduction for bi-intuitionistic logic.Luca Tranchini - 2017 - Journal of Applied Logic 25:S72-S96.
References found in this work
An Algebraic and Kripke-Style Approach to a Certain Extension of Intuitionistic Logic.Cecylia Rauszer - 1980 - [Available From Ars Polona].
Constructive negation, implication, and co-implication.Heinrich Wansing - 2008 - Journal of Applied Non-Classical Logics 18 (2-3):341-364.
The method of hypersequents in the proof theory of propositional non-classical logics.Arnon Avron - 1996 - In Wilfrid Hodges (ed.), Logic: Foundations to Applications. Oxford: pp. 1-32.