Gentzen-Type Sequent Calculi for Extended Belnap–Dunn Logics with Classical Negation: A General Framework

Logica Universalis:1-27 (forthcoming)
Gentzen-type sequent calculi GBD+, GBDe, GBD1, and GBD2 are respectively introduced for De and Omori’s axiomatic extensions BD+, BDe, BD1, and BD2 of Belnap–Dunn logic by adding classical negation. These calculi are constructed based on a small modification of the original characteristic axiom scheme for negated implication. Theorems for syntactically and semantically embedding these calculi into a Gentzen-type sequent calculus LK for classical logic are proved. The cut-elimination, decidability, and completeness theorems for these calculi are obtained using these embedding theorems. Similar results excluding cut-elimination results are also obtained for alternative Gentzen-type sequent calculi gBD+, gBDe, gBD1, and gBD2 for BD+, BDe, BD1, and BD2, respectively. These alternative calculi are constructed based on the original characteristic axiom scheme for negated implication.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1007/s11787-018-0218-3
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 36,555
External links

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

A Useful Four-Valued Logic.N. D. Belnap - 1977 - In J. M. Dunn & G. Epstein (eds.), Modern Uses of Multiple-Valued Logic. D. Reidel.
Constructible Falsity and Inexact Predicates.Ahmad Almukdad & David Nelson - 1984 - Journal of Symbolic Logic 49 (1):231-233.

View all 16 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Gentzen-Type Methods for Bilattice Negation.Norihiro Kamide - 2005 - Studia Logica 80 (2-3):265-289.
Proof Theory of Paraconsistent Quantum Logic.Norihiro Kamide - 2018 - Journal of Philosophical Logic 47 (2):301-324.
Symmetric and Dual Paraconsistent Logics.Norihiro Kamide & Heinrich Wansing - 2010 - Logic and Logical Philosophy 19 (1-2):7-30.
Sequent Calculi for Some Trilattice Logics.Norihiro Kamide & Heinrich Wansing - 2009 - Review of Symbolic Logic 2 (2):374-395.
A Survey of Nonstandard Sequent Calculi.Andrzej Indrzejczak - 2014 - Studia Logica 102 (6):1295-1322.
A Hierarchy of Weak Double Negations.Norihiro Kamide - 2013 - Studia Logica 101 (6):1277-1297.
Cut as Consequence.Curtis Franks - 2010 - History and Philosophy of Logic 31 (4):349-379.
A Gentzen Calculus for Nothing but the Truth.Stefan Wintein & Reinhard Muskens - 2016 - Journal of Philosophical Logic 45 (4):451-465.
LEt ® , LR °[^( ~ )], LK and Cutfree Proofs.Katalin Bimbó - 2007 - Journal of Philosophical Logic 36 (5):557-570.


Added to PP index

Total downloads
4 ( #797,932 of 2,302,572 )

Recent downloads (6 months)
4 ( #152,928 of 2,302,572 )

How can I increase my downloads?

Monthly downloads

My notes

Sign in to use this feature