Abstract

This study introduces and investigates a Gentzen-style sequent calculus, sQBDi, for Niki and Omori’s extended first-order intuitionistic Belnap–Dunn logic, QBDi. The propositional fragment of QBDi is an intuitionistic variant of De and Omori’s extended Belnap–Dunn logic, BD+, with classical negation. The intuitionistic-negation-less propositional fragment of QBDi is an intuitionistic variant of Avron’s self-extensional paraconsistent four-valued logic, SE4. In this study, the cut-elimination, Kripke completeness, and Craig interpolation theorems for sQBDi are proved through several theorems concerning syntactical and semantical embeddings of sQBDi into a Gentzen-style sequent calculus for first-order intuitionistic logic. The paraconsistent and constructive properties of sQBDi are also derived. This study also provides some comparisons, including one between sQBDi (which follows the American plan for negation) and Moisil–Leitgeb’s HYPE (which follows the Australian plan for negation).