David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jack Alan Reynolds
Learn more about PhilPapers
Bi-intuitionistic logic is the union of intuitionistic and dual intuitionistic logic, and was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent ‘cut-free’ sequent calculus has recently been shown to fail cut-elimination. We present a new cut-free sequent calculus for bi-intuitionistic logic, and prove it sound and complete with respect to its Kripke semantics. Ensuring completeness is complicated by the interaction between intuitionistic implication and dual intuitionistic exclusion, similarly to future and past modalities in tense logic. Our calculus handles this interaction using derivations and refutations as first class citizens. We employ extended sequents which pass information from premises to conclusions using variables instantiated at the leaves of refutations, and rules which compose certain refutations and derivations to form derivations. Automated deduction using terminating backward search is also possible, although this is not our main purpose.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library||
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Rajeev Gore, Linda Postniece & Alwen Tiu, Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents.
Roy Dyckhoff & Luis Pinto (1998). Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic. Studia Logica 60 (1):107-118.
Carl J. Posy (1982). A Free IPC is a Natural Logic: Strong Completeness for Some Intuitionistic Free Logics. Topoi 1 (1-2):30-43.
Mauro Ferrari (1997). Cut-Free Tableau Calculi for Some Intuitionistic Modal Logics. Studia Logica 59 (3):303-330.
Jan von Plato (2012). Gentzen's Proof Systems: Byproducts in a Work of Genius. Bulletin of Symbolic Logic 18 (3):313-367.
Roy Dyckhoff & Sara Negri (2000). Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic Logic. Journal of Symbolic Logic 65 (4):1499-1518.
Giambattista Amati, Luigia Carlucci-Aiello & Fiora Pirri (1997). Intuitionistic Autoepistemic Logic. Studia Logica 59 (1):103-120.
Wil Dekkers, Martin Bunder & Henk Barendregt (1998). Completeness of the Propositions-as-Types Interpretation of Intuitionistic Logic Into Illative Combinatory Logic. Journal of Symbolic Logic 63 (3):869-890.
Kai Brünnler (2006). Cut Elimination Inside a Deep Inference System for Classical Predicate Logic. Studia Logica 82 (1):51 - 71.
Sara Negri (2002). Varieties of Linear Calculi. Journal of Philosophical Logic 31 (6):569-590.
Branislav R. Boričić (1986). A Cut-Free Gentzen-Type System for the Logic of the Weak Law of Excluded Middle. Studia Logica 45 (1):39 - 53.
Enrico Martino (1998). Negationless Intuitionism. Journal of Philosophical Logic 27 (2):165-177.
Norihiro Kamide (2006). Phase Semantics and Petri Net Interpretation for Resource-Sensitive Strong Negation. Journal of Logic, Language and Information 15 (4):371-401.
Added to index2010-09-22
Total downloads9 ( #363,552 of 1,906,942 )
Recent downloads (6 months)1 ( #468,570 of 1,906,942 )
How can I increase my downloads?