Bi-Classical Connexive Logic and its Modal Extension: Cut-elimination, completeness and duality

Norihiro Kamide

doi:10.12775/LLP.2019.002

Authors

Norihiro Kamide Teikyo University http://orcid.org/0000-0001-7736-8055

DOI:

https://doi.org/10.12775/LLP.2019.002

Keywords

bi-classical connexive logic, sequent calculus, cut-elimination, duality, completeness

Abstract

In 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.

Author Biography

Norihiro Kamide, Teikyo University

Faculty of Science and Engineering, Department of Information and Electronic Engineering

References

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.