Unified Gentzen Approach to Connexive Logics over Wansing's C

TL;DR

This paper develops Gentzen-style sequent calculi and natural deduction systems for a family of connexive logics over Wansing's basic logic C, incorporating classical principles and proving key properties like equivalence, cut-elimination, and normalization.

Contribution

It introduces a unified Gentzen approach for connexive logics over Wansing's C, including new calculi and proof of their fundamental properties.

Findings

Proposed sequent calculi are equivalent to natural deduction systems.

Cut-elimination and normalization theorems are established.

The framework unifies connexive logics with classical principles.

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 connexive logic C. The C-family is derived from C by incorporating the Peirce law, the law of excluded middle, and the generalized law of excluded middle. Theorems establishing 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.