Paraconsistent Double Negation That Can Simulate Classical Negation

A new classical paraconsistent logic (CP), which is a variant of Nelson's paraconsistent four-valued logic, is introduced as a Gentzen-type sequent calculus. The logic CP can simulate the classical negation in classical logic by paraconsistent double negation in CP. Some 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.