An Extended Paradefinite Logic Combining Conflation, Paraconsistent Negation, Classical Negation, and Classical Implication: How to Construct Nice Gentzen-type Sequent Calculi

In this study, an extended paradefinite logic with classical negation (EPLC), which has the connectives of conflation, paraconsistent negation, classical negation, and classical implication, is introduced as a Gentzen-type sequent calculus. The logic EPLC is regarded as a modification of Arieli, Avron, and Zamansky's ideal four-valued paradefinite logic (4CC) and as an extension of De and Omori's extended Belnap-Dunn logic with classical negation (BD+) and Avron's self-extensional four-valued paradefinite logic (SE4). The completeness, cut-elimination, and decidability theorems for EPLC are proved and EPLC is shown to be embeddable into classical logic. The strong equivalence substitution property and the admissibilities of the rules of negative symmetry, contraposition, and involution are shown for EPLC. Some alternative simple Gentzen-type sequent calculi, which are theorem-equivalent to EPLC, are obtained via these characteristic properties.

Automated summary

In this study, an extended paradefinite logic with classical negation (EPLC) is introduced and its completeness, cut-elimination, and decidability theorems are proved. Additionally, some important properties of EPLC are shown.