Pokaż uproszczony rekord

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

dc.contributor.authorKamide, Norihiro
dc.date.accessioned2025-12-12T15:22:21Z
dc.date.available2025-12-12T15:22:21Z
dc.date.issued2025-07-02
dc.identifier.issn0138-0680
dc.identifier.urihttp://hdl.handle.net/11089/56965
dc.description.abstractGentzen-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.en
dc.language.isoen
dc.publisherWydawnictwo Uniwersytetu Łódzkiegopl
dc.relation.ispartofseriesBulletin of the Section of Logic;2en
dc.rights.urihttps://creativecommons.org/licenses/by-nc-nd/4.0
dc.subjectconnexive logicen
dc.subjectcut-elimination theoremen
dc.subjectnormalization theoremen
dc.titleCut-elimination and Normalization Theorems for Connexive Logics over Wansing’s Cen
dc.typeArticle
dc.page.number157-205
dc.contributor.authorAffiliationNagoya City University, Graduate School of Data Scienceen
dc.identifier.eissn2449-836X
dc.referencesH. 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/1093636101en
dc.referencesA. 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/2274105en
dc.referencesR. Angell, A propositional logics with subjunctive conditionals, Journal of Symbolic Logic, vol. 27 (1962), pp. 327–343, DOI: https://doi.org/10.2307/2964651en
dc.referencesJ. 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-010en
dc.referencesH. B. Curry, Foundations of mathematical logic, McGraw-Hill, New York (1963).en
dc.referencesP. É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-7en
dc.referencesW. 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.en
dc.referencesM. 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-Gen
dc.referencesN. Francez, Natural deduction for two connexive logics, IfCoLog Journal of Logics and their Applications, vol. 3(3) (2016), pp. 479–504.en
dc.referencesL. 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/BF02017499en
dc.referencesY. Gurevich, Intuitionistic logic with strong negation, Studia Logica 36, vol. 36 (1977), pp. 49–59.en
dc.referencesN. Kamide, Cut-free single-succedent systems revisited, Bulletin of the Section of Logic, vol. 34(3) (2005), pp. 165–175.en
dc.referencesN. 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-435en
dc.referencesN. 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-3en
dc.referencesN. 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-6en
dc.referencesN. 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.19en
dc.referencesN. 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.en
dc.referencesN. 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.001en
dc.referencesN. 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-9en
dc.referencesN. Kamide, H. Wansing, Completeness of connexive Heyting-Brouwer logic, IFCoLog Journal of Logics and their Applications, vol. 3(3) (2016), pp. 441–466.en
dc.referencesN. Kürbis, Y. Petrukhin, Normalisation for some quite interesting many-valued logics, Logic and Logical Philosophy, vol. 30(3) (2021), pp. 493–534.en
dc.referencesS. McCall, Connexive implication, Journal of Symbolic Logic, vol. 31 (1966), pp. 415–433, DOI: https://doi.org/10.2307/2270458en
dc.referencesS. Negri, J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge (2001), DOI: https://doi.org/10.1017/CBO9780511527340en
dc.referencesD. Nelson, Constructible falsity, Journal of Symbolic Logic, vol. 14 (1949), pp. 16–26, DOI: https://doi.org/10.2307/2268973en
dc.referencesS. Niki, Intuitionistic views on connexive constructible falsity, Journal of Applied Logics, vol. 11(2) (2024), pp. 125–157.en
dc.referencesS. 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-4en
dc.referencesG. 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.en
dc.referencesG. 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.en
dc.referencesH. 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_8en
dc.referencesH. 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).en
dc.referencesD. Prawitz, Natural deduction: a proof-theoretical study, Almqvist and Wiksell, Stockholm (1965), DOI: https://doi.org/10.2307/2271676en
dc.referencesW. Rautenberg, Klassische und nicht-klassische Aussagenlogik, Vieweg+Teubner Verlag, Wiesbaden (1979), DOI: https://doi.org/10.1007/978-3-322-85796-5en
dc.referencesP. 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/2274279en
dc.referencesM. 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/2272429en
dc.referencesA. 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/1038949541en
dc.referencesJ. von Plato, Proof theory of full classical propositional logic (1999), manuscript, 16 pages.en
dc.referencesJ. 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/s001530100091en
dc.referencesN. Vorob’ev, A constructive propositional calculus with strong negation (in Russian), Doklady Akademii Nauk SSSR, vol. 85 (1952), pp. 465–468.en
dc.referencesH. 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-8en
dc.referencesH. 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.en
dc.referencesH. 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/EXT035en
dc.referencesH. 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.en
dc.referencesH. Wansing, Connexive Logic, [in:] E. N. Zalta, U. Nodelman (eds.), The Stanford Encyclopedia of Philosophy, Summer 2023 ed., Metaphysics Research Lab, Stanford University (2023).en
dc.referencesE. 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-1en
dc.contributor.authorEmaildrnkamide08@kpd.biglobe.ne.jp
dc.identifier.doi10.18778/0138-0680.2025.04
dc.relation.volume54


Pliki tej pozycji

Thumbnail
Nazwa:
157-205_Kamide.pdf
Rozmiar:
1.574MB
Format:
PDF
Oglądaj/Otwórz

Pozycja umieszczona jest w następujących kolekcjach

Pokaż uproszczony rekord

https://creativecommons.org/licenses/by-nc-nd/4.0
Poza zaznaczonymi wyjątkami, licencja tej pozycji opisana jest jako https://creativecommons.org/licenses/by-nc-nd/4.0