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 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar DOI: https://doi.org/10.1215/00294527-2008-010

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

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
Google Scholar 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.
Google Scholar 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
Google Scholar 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.
Google Scholar

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
Google Scholar DOI: https://doi.org/10.1007/BF02017499

Y. Gurevich, Intuitionistic logic with strong negation, Studia Logica 36, vol. 36 (1977), pp. 49–59.
Google Scholar 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.
Google Scholar

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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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.
Google Scholar

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
Google Scholar 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
Google Scholar 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.
Google Scholar

N. Kürbis, Y. Petrukhin, Normalisation for some quite interesting many-valued logics, Logic and Logical Philosophy, vol. 30(3) (2021), pp. 493–534.
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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.
Google Scholar

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
Google Scholar 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.
Google Scholar

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.
Google Scholar

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
Google Scholar 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).
Google Scholar

D. Prawitz, Natural deduction: a proof-theoretical study, Almqvist and Wiksell, Stockholm (1965), DOI: https://doi.org/10.2307/2271676
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar DOI: https://doi.org/10.1305/ndjfl/1038949541

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

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
Google Scholar 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.
Google Scholar

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
Google Scholar 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.
Google Scholar

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
Google Scholar 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.
Google Scholar

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).
Google Scholar

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
Google Scholar DOI: https://doi.org/10.1016/S0304-3975(01)00296-1