Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Unified Gentzen Approach to Connexive Logics over Wansing's C

Norihiro Kamide

TL;DR

This work develops a unified Gentzen-style proof-theoretic framework for a family of connexive logics over Wansing's C, incorporating the Excluded Middle, Peirce's Law, and the Generalized Excluded Middle to cover C, C3, MC, and CN. It defines corresponding sequent calculi (sC, sC3, sMC, sCN) and natural deduction systems (nC, nC3, nMC, nCN), including generalized and starred variants, and proves strong correspondences between the two formalisms. The main meta-results include cut-elimination for the sequent calculi and normalization for the natural deduction systems, together with a separation theorem showing the four logics are not all logically equivalent. By embedding sMC into a classical-style framework LJ+ with Peirce and establishing uniform translation principles, the work provides a coherent, interchangeable foundation for analyzing connexive logics and supports formal automation and philosophical analysis.

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.

Unified Gentzen Approach to Connexive Logics over Wansing's C

TL;DR

This work develops a unified Gentzen-style proof-theoretic framework for a family of connexive logics over Wansing's C, incorporating the Excluded Middle, Peirce's Law, and the Generalized Excluded Middle to cover C, C3, MC, and CN. It defines corresponding sequent calculi (sC, sC3, sMC, sCN) and natural deduction systems (nC, nC3, nMC, nCN), including generalized and starred variants, and proves strong correspondences between the two formalisms. The main meta-results include cut-elimination for the sequent calculi and normalization for the natural deduction systems, together with a separation theorem showing the four logics are not all logically equivalent. By embedding sMC into a classical-style framework LJ+ with Peirce and establishing uniform translation principles, the work provides a coherent, interchangeable foundation for analyzing connexive logics and supports formal automation and philosophical analysis.

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.
Paper Structure (3 sections, 12 theorems, 1 equation)

This paper contains 3 sections, 12 theorems, 1 equation.

Table of Contents

  1. Introduction
  2. Gentzen-style sequent calculi
  3. Gentzen-style natural deduction systems

Key Result

Proposition 2.3

Let $L$ be LJ$^+$, sC, sC3, sMC, or sCN. For any formula $\hbox{\it $\alpha$}$ and any set $\hbox{\it $\Gamma$}$ of formulas, we have: $L$$\vdash$$\hbox{\it $\alpha$}, \hbox{\it $\Gamma$} \Rightarrow \hbox{\it $\alpha$}$.

Theorems & Definitions (22)

  • Definition 2.1: LJ$^+$, sC, sC3, sMC, and sCN
  • Remark 2.2
  • Proposition 2.3
  • Proposition 2.4
  • Theorem 2.5: Cut-elimination for LJ$^+$ and sC GENTZENWANSINGAIML2005
  • Theorem 2.6: Cut-elimination for sC3, sMC, and sCN
  • Theorem 2.7: Separation of C, C3, MC, and CN
  • Definition 2.8: sMC$^*$ and sCN$^*$
  • Remark 2.9
  • Proposition 2.10
  • ...and 12 more