Unified Gentzen-Style Sequent Calculi and Natural Deduction for Connexive Logics
A single Gentzen-style framework that treats sequent calculus and natural deduction uniformly for the C-family of connexive logics — Wansing's basic constructive connexive logic C and its extensions C3, MC, and CN, obtained by adding the law of excluded middle, Peirce's law, and a generalized excluded middle rule. It establishes equivalence between each sequent calculus and its natural deduction counterpart, and proves cut-elimination for the calculi and normalization for the deduction systems.
2501.00498
Connexive logics are paraconsistent logics distinguished by validating Boethius' theses linking implication and negation. This paper builds a single Gentzen-style framework that treats sequent calcul…