Cut-elimination and Normalization Theorems for Connexive Logics over Wansing’s C

Abstract

Gentzen-style sequent calculi and Gentzen-style natural deduction systems are introduced for a family (C-family) of connexive logics over Wansing’s basic constructive connexive logic C. The C-family is derived from C by incorporating Peirce’s law, the law of excluded middle, and the generalized law of excluded middle. Natural deduction systems with general elimination rules are also introduced for the C-family. Theorems establishing the equivalence between the proposed sequent calculi and natural deduction systems are demonstrated. Cut-elimination and normalization theorems are established for the proposed sequent calculi and natural deduction systems, respectively. Additionally, similar results are obtained for a family (N-family) of paraconsistent logics over Nelson’s constructive four-valued logic N4.