Paraconsistent Double Negations as Classical and Intuitionistic Negations

摘要

AbstractA classical paraconsistent logic (CP), which is regarded as a modified extension of first-degree entailment logic, is introduced as a Gentzen-type sequent calculus. This logic can simulate the classical negation in classical logic by paraconsistent double negation in CP. Theorems for syntactically and semantically embedding CP into a Gentzen-type sequent calculus LK for classical logic and vice versa are proved. The cut-elimination and completeness theorems for CP are also shown using these embedding theorems. Similar results are also obtained for an intuitionistic paraconsistent logic (IP), and several versions of Glivenko and G?del-Gentzen translation theorems are proved for CP and IP.