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

Norihiro Kamide

doi:10.18778/0138-0680.2025.04

Authors

Norihiro Kamide Nagoya City University, Graduate School of Data Science Author https://orcid.org/0000-0001-7736-8055

DOI:

https://doi.org/10.18778/0138-0680.2025.04

Keywords:

connexive logic, cut-elimination theorem, normalization theorem

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.

References

H. Africk, Classical logic, intuitionistic logic, and the Peirce rule, Notre Dame Journal of Formal Logic, vol. 33(2) (1992), pp. 229–235, DOI: https://doi.org/10.1305/ndjfl/1093636101 DOI: https://doi.org/10.1305/ndjfl/1093636101

A. Almukdad, D. Nelson, Constructible falsity and inexact predicates, Journal of Symbolic Logic, vol. 49(1) (1984), pp. 231–233, DOI: https://doi.org/10.2307/2274105 DOI: https://doi.org/10.2307/2274105

R. Angell, A propositional logics with subjunctive conditionals, Journal of Symbolic Logic, vol. 27 (1962), pp. 327–343, DOI: https://doi.org/10.2307/2964651 DOI: https://doi.org/10.2307/2964651

J. Cantwell, The logic of conditional negation, Notre Dame Journal of Formal Logic, vol. 49 (2008), pp. 245–260, DOI: https://doi.org/10.1215/00294527-2008-010 DOI: https://doi.org/10.1215/00294527-2008-010

H. B. Curry, Foundations of mathematical logic, McGraw-Hill, New York (1963).

P. Égré, L. Rossi, J. Sprenger, De finettian logics of indicative conditionals Part II: Proof theory and algebraic semantics, Journal of Philosophical Logic, vol. 50 (2021), pp. 215–247, DOI: https://doi.org/10.1007/S10992-020-09572-7 DOI: https://doi.org/10.1007/s10992-020-09572-7

W. Felscher, Kombinatorische Konstruktionen mit Beweisen und Schnittelimination, [in:] J. Diller, G. H. Müller (eds.), ⊨ ISILC Proof Theory Symposion, Springer Berlin Heidelberg, Berlin, Heidelberg (1975), pp. 119–151. DOI: https://doi.org/10.1007/BFb0079549

M. Fitting, Bilattices and the semantics of logic programming, The Journal of Logic Programming, vol. 11(2) (1991), pp. 91–116, DOI: https://doi.org/10.1016/0743-1066(91)90014-G DOI: https://doi.org/10.1016/0743-1066(91)90014-G

N. Francez, Natural deduction for two connexive logics, IfCoLog Journal of Logics and their Applications, vol. 3(3) (2016), pp. 479–504.

L. Gordeev, On cut elimination in the presence of Peirce rule, Archiv für Mathematische Logik und Grundlagenforsch, vol. 26 (1987), pp. 147–164, DOI: https://doi.org/10.1007/BF02017499 DOI: https://doi.org/10.1007/BF02017499

Y. Gurevich, Intuitionistic logic with strong negation, Studia Logica 36, vol. 36 (1977), pp. 49–59. DOI: https://doi.org/10.1007/BF02121114

N. Kamide, Cut-free single-succedent systems revisited, Bulletin of the Section of Logic, vol. 34(3) (2005), pp. 165–175.

N. Kamide, Natural deduction systems for Nelson’s paraconsistent logic and its neighbors, Journal of Applied Non-Classical Logics, vol. 15(4) (2005), pp. 405–435, DOI: https://doi.org/10.3166/JANCL.15.405-435 DOI: https://doi.org/10.3166/jancl.15.405-435

N. Kamide, Embedding friendly first-order paradefinite and connexive logics, Journal of Philosophical logic, vol. 51(5) (2022), pp. 1055–1102, DOI: https://doi.org/10.1007/S10992-022-09659-3 DOI: https://doi.org/10.1007/s10992-022-09659-3

N. Kamide, Rules of explosion and excluded middle: Constructing a unified single-succedent Gentzen-style framework for classical, paradefinite, paraconsistent, and paracomplete logics, Journal of Logic, Language and Information, vol. 33(2) (2024), pp. 143–178, DOI: https://doi.org/10.1007/s10849-024-09416-6 DOI: https://doi.org/10.1007/s10849-024-09416-6

N. Kamide, Unified Gentzen approach to connexive logics over Wansing’s C, [in:] A. Indrzejczak, M. Zawidzki (eds.), Proceedings of the 11th International Conference on Non-Classical Logics – Theory and Applications (NCL’24), vol. 415 of Electronic Proceedings in Theoretical Computer Science (2024), pp. 214–228, DOI: https://doi.org/10.4204/EPTCS.415.19 DOI: https://doi.org/10.4204/EPTCS.415.19

N. Kamide, H. Wansing, Connexive modal logic based on positive S4, [in:] J.-Y. Beziau, M. E. Coniglio (eds.), Logic without Frontiers: Festschrift for Walter Alexandre Carnielli on the occasion of his 60th Birthday, vol. 17 of Tribute Series, College Publications, London (2011), pp. 389–410.

N. Kamide, H. Wansing, Proof theory of Nelson’s paraconsistent logic: A uniform perspective, Theoretical Computer Science, vol. 415 (2012), pp. 1–38, DOI: https://doi.org/10.1016/J.TCS.2011.11.001 DOI: https://doi.org/10.1016/j.tcs.2011.11.001

N. Kamide, H. Wansing, Proof theory of N4-related paraconsistent logics, vol. 54 of Studies in Logic, College Publications, London (2015), DOI: https://doi.org/10.1007/s11225-017-9729-9 DOI: https://doi.org/10.1007/s11225-017-9729-9

N. Kamide, H. Wansing, Completeness of connexive Heyting-Brouwer logic, IFCoLog Journal of Logics and their Applications, vol. 3(3) (2016), pp. 441–466.

N. Kürbis, Y. Petrukhin, Normalisation for some quite interesting many-valued logics, Logic and Logical Philosophy, vol. 30(3) (2021), pp. 493–534. DOI: https://doi.org/10.12775/LLP.2021.009

S. McCall, Connexive implication, Journal of Symbolic Logic, vol. 31 (1966), pp. 415–433, DOI: https://doi.org/10.2307/2270458 DOI: https://doi.org/10.2307/2270458

S. Negri, J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge (2001), DOI: https://doi.org/10.1017/CBO9780511527340 DOI: https://doi.org/10.1017/CBO9780511527340

D. Nelson, Constructible falsity, Journal of Symbolic Logic, vol. 14 (1949), pp. 16–26, DOI: https://doi.org/10.2307/2268973 DOI: https://doi.org/10.2307/2268973

S. Niki, Intuitionistic views on connexive constructible falsity, Journal of Applied Logics, vol. 11(2) (2024), pp. 125–157.

S. Niki, H. Wansing, On the provable contradictions of the connexive logics C and C3, Journal of Philosophical Logic, vol. 52(5) (2023), pp. 1355–1383, DOI: https://doi.org/10.1007/S10992-023-09709-4 DOI: https://doi.org/10.1007/s10992-023-09709-4

G. K. Olkhovikov, On a new three-valued paraconsistent logic, [in:] Logic of Law and Tolerance, Ural State University Press, Yekaterinburg (2002), pp. 96–113, it was translated by T.M. Ferguson in IfCoLog Journal of Logics and their Applications 3(3), pp. 317–334, 2016.

G. K. Olkhovikov, A complete, correct, and independent axiomatization of the first-order fragment of a three-valued paraconsistent logic, IfCoLog Journal of Logics and their Applications, vol. 3(3) (2016), pp. 335–340.

H. Omori, From paraconsistent logic to dialetheic logic, [in:] H. Andreas, P. Verdee (eds.), Logical Studies of Paraconsistent Reasoning in Science and Mathematics, Springer, Berlin (2016), pp. 111–134, DOI: https://doi.org/10.1007/978-3-319-40220-8_8 DOI: https://doi.org/10.1007/978-3-319-40220-8_8

H. Omori, H. Wansing, An extension of connexive logic C, [in:] N. Olivetti, R. Verbrugge, S. Negri, G. Sandu (eds.), Advances in Modal Logic 13, College Publications, London (2020).

D. Prawitz, Natural deduction: a proof-theoretical study, Almqvist and Wiksell, Stockholm (1965), DOI: https://doi.org/10.2307/2271676 DOI: https://doi.org/10.2307/2271676

W. Rautenberg, Klassische und nicht-klassische Aussagenlogik, Vieweg+Teubner Verlag, Wiesbaden (1979), DOI: https://doi.org/10.1007/978-3-322-85796-5 DOI: https://doi.org/10.1007/978-3-322-85796-5

P. Schroeder-Heister, A natural extension of natural deduction, Journal of Symbolic Logic, vol. 49(4) (1984), pp. 1284–1300, DOI: https://doi.org/10.2307/2274279 DOI: https://doi.org/10.2307/2274279

M. E. Szabo (ed.), Collected papers of Gerhard Gentzen, Studies in Logic and the Foundations of Mathematics, North-Holland (1969), DOI: https://doi.org/10.2307/2272429 DOI: https://doi.org/10.2307/2272429

A. M. Tamminga, K. Tanaka, A natural deduction system for first degree entailment, Notre Dame Journal of Formal Logic, vol. 40(2) (1999), pp. 258–272, DOI: https://doi.org/10.1305/NDJFL/1038949541 DOI: https://doi.org/10.1305/ndjfl/1038949541

J. von Plato, Proof theory of full classical propositional logic (1999), manuscript, 16 pages.

J. von Plato, Natural deduction with general elimination rules, Archive for Mathematical Logic, vol. 40(7) (2001), pp. 541–567, DOI:https://doi.org/10.1007/s001530100091 DOI: https://doi.org/10.1007/s001530100091

N. Vorob’ev, A constructive propositional calculus with strong negation (in Russian), Doklady Akademii Nauk SSSR, vol. 85 (1952), pp. 465–468.

H. Wansing, The logic of information structures, vol. 681 of Lecture Notes in Artificial Intelligence, Springer, Berlin, Heidelberg (1993), DOI: https://doi.org/10.1007/3-540-56734-8 DOI: https://doi.org/10.1007/3-540-56734-8

H. Wansing, Connexive modal logic, [in:] R. Schmidt, I. Pratt-Hartmann, M. Reynolds, H. Wansing (eds.), Advances in Modal Logic 5, King’s College Publications, London (2005), pp. 367–385.

H. Wansing, Falsification, natural deduction and bi-intuitionistic logic, Journal of Logic and Computation, vol. 26(1) (2016), pp. 425–450, DOI: https://doi.org/10.1093/LOGCOM/EXT035 DOI: https://doi.org/10.1093/logcom/ext035

H. Wansing, Natural deduction for bi-connexive logic and a two-sorted typed λ-calculus, IfCoLog Journal of Logics and their Applications, vol. 3(3) (2016), pp. 413–440.

H. Wansing, Connexive Logic, [in:] E. N. Zalta, U. Nodelman (eds.), The Stanford Encyclopedia of Philosophy, Summer 2023 ed., Metaphysics Research Lab, Stanford University (2023).

E. Zimmermann, Peirce’s rule in natural deduction, Theoretical Computer Science, vol. 275 (2002), pp. 561–574, DOI: https://doi.org/10.1016/S0304-3975(01)00296-1 DOI: https://doi.org/10.1016/S0304-3975(01)00296-1