Bi-Classical Connexive Logic and its Modal Extension: Cut-elimination, completeness and duality
Keywordsbi-classical connexive logic, sequent calculus, cut-elimination, duality, completeness
AbstractIn this study, a new paraconsistent four-valued logic called bi-classical connexive logic (BCC) is introduced as a Gentzen-type sequent calculus. Cut-elimination and completeness theorems for BCC are proved, and it is shown to be decidable. Duality property for BCC is demonstrated as its characteristic property. This property does not hold for typical paraconsistent logics with an implication connective. The same results as those for BCC are also obtained for MBCC, a modal extension of BCC.
Almukdad, A„ and D. Nelson, “Constructible falsity and inexact predicates”, Journal of Symbolic Logic 49. 1 (1984): 231–233. DOI: http://dx.doi.org/10.2307/2274105
Angell, R., “A propositional logics with subjunctive conditionals”, Journal of Symbolic Logic 27, 3 (1962): 327–343. DOI: http://dx.doi.org/10.2307/2964651
Belnap, N.D., “A useful four-valued logic”, pages 5–37 in G. Epstein and J.M. Dunn (eds.), Modern Uses of Multiple-Valued Logic, Dordrecht, Reidel, 1977.
Belnap, N.D., “How a computer should think”, pages 30–56 in G. Ryle (ed.), Contemporary Aspects of Philosophy, Oriel Press, Stocksfield, 1977.
Buisman, L.. and R. Goré, “A cut-free sequent calculus for bi-intuitionistic logic”, pages 90–106 in Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2007), Lecture Notes in Artificial Intelligence 4545, 2007. DOI: http://dx.doi.org/10.1007/978-3-540-73099-6_9
Dunn, J.M., “Intuitive semantics for first-degree entailment and ‘coupled trees’”, Philosophical Studies 29, 3 (1976): 149–168.
Ferguson, T.M., “On arithmetic formulated connexively”, IFCoLoG Journal of Logics and their Applications 3, 3 (2016): 357–376.
Francez, N., “Natural deduction for two connexive logics”, IFCoLoG Journal of Logics and their Applications 3, 3 (2016): 479–504.
Gurevich, Y., “Intuitionistic logic with strong negation”, Studia Logica 36, 1–2 (1977): 49–59. DOI: http://dx.doi.org/10.1007/BF02121114
Kamide, N., “Cut-free systems for restricted bi-intuitionistic logic and its connexive extension”, pages 137–142 Proceedings of the 46th International Symposium on Multiple-Valued Logic (ISMVL 2016), 2016. DOI: http://dx.doi.org/10.1109/ISMVL.2016.11
Kamide, N., and H. Wansing, “Symmetric and dual paraconsistent logics”, Logic and Logical Philosophy 19, 1–2 (2010): 7–30. DOI: http://dx.doi.org/10.12775/LLP.2010.002
Kamide, N., and H. Wansing, “Connexive modal logic based on positive S4”, pages 389–410 in J.-Y. Beziau and M. Esteban 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.
Kamide, N., and H. Wansing, “Proof theory of N4-related paraconsistent logics”, Studies in Logic 54, College Publications, 2015. http://dx.doi.org/DOI: 10.1007/s11225-017-9729-9
Kamide, N., and H. Wansing, “Completeness of connexive Heyting-Brouwer logic”, IFCoLog Journal of Logics and their Applications 3, 3 (2016): 441–466.
Łukowsli, P., “Modal interpretation of Heyting-Brouwer logic”, Bulletin of the Section of Logic 25, 2 (1996): 80–83.
Łukowsli, P., “A deductive-reductive form of logic: Intuitionistic S4 modalities”, Logic and Logical Philosophy 10 (2002): 79–91. DOI: http://dx.doi.org/10.12775/LLP.2002.005
McCall, S., “Connexive implication”, Journal of Symbolic Logic 31 (1966): 415–433. DOI: http://dx.doi.org/10.2307/2270458
Nelson, D., “Constructible falsity”, Journal of Symbolic Logic 14, 1 (1949): 16–26. DOI: http://dx.doi.org/10.2307/2268973
Omori, H., “From paraconsistent logic to dialetheic logic”, pages 111–134 in H. Andreas and P. Verdée (eds.), Logical Studies of Paraconsistent Reasoning in Science and Mathematics, Trends in Logic 45, 2016. DOI: http://dx.doi.org/10.1007/978-3-319-40220-8_8
Omori, H., “A simple connexive extension of the basic relevant logic BD”, IFCoLoG Journal of Logics and their Applications 3, 3 (2016): 467–478.
Omori, H., and H. Wansing, “A web site on connexive logic”, 2015. https://sites.google.com/site/connexivelogic/home
Pinto, L., and T. Uustalu, “Relating sequent calculi for bi-intuitionistic propositional logic”, pages 57–72 in Proceedings of the 3rd International Workshop on Classical Logic and Computation (CL & C 2010), 2010. DOI: http://dx.doi.org/10.4204/EPTCS.47.7
Postniece, L., “Proof theory and proof search of bi-intuitionistic and tense logic”, PhD thesis, The Australian National University, Canberra, 2010.
Rauszer, C., “A formalization of the propositional calculus of H-B logic”, Studia Logica 33, 1 (1974): 23–34. DOI: http://dx.doi.org/10.1007/BF02120864
Rauszer, C., “Applications of Kripke models to Heyting-Brouwer logic”, Studia Logica 36, 1–2 (1977): 61–71. DOI: http://dx.doi.org/10.1007/BF02121115
Rauszer, C., “An algebraic and Kripke-style approach to a certain extension of intuitionistic logic”, pages 1–67 in Dissertations Mathematicae, Polish Scientific Publishers, 1980.
Rautenberg, W., Klassische und nicht-klassische Aussagenlogik’, Vieweg, Braunschweig, 1979.
Troelstra, A.S., and H. Schwichtenberg, Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science 45, Second Edition, Cambridge University Press, 2000. DOI: http://dx.doi.org/10.1017/CBO9781139168717
Vorob’ev, N.N., “A constructive propositional calculus with strong negation” (in Russian), Doklady Akademii Nauk SSR 85 (1952): 465–468.
Wansing, H., “Connexive modal logic”, pages 367–385 in Advances in Modal Logic, vol. 5, 2005.
Wansing, H., “Constructive negation, implication, and co-implication”, Journal of Applied Non-Classical Logics 18 (2008): 341–364. DOI: http://dx.doi.org/10.3166/jancl.18.341-364
Wansing, H., “Falsification, natural deduction and bi-intuitionistic logic”, Journal of Logic and Computation 26, 1 (2016): 425–450. DOI: http://dx.doi.org/10.1093/logcom/ext035
Wansing, H., “Connexive logic”, Stanford Encyclopedia of Philosophy, 2014. http://plato.stanford.edu/entries/logic-connexive/
Wansing, H., “Natural deduction for bi-connexive logic and a two-sorted typed λ-calculus”, IfCoLog Journal of Logics and their Applications 3, 3 (2016): 413–439.
How to Cite
Number of views and downloads: 277
Number of citations: 1