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

Norihiro Kamide



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.


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

Full Text:



Almukdad, A„ and D. Nelson, “Constructible falsity and inexact predicates”, Journal of Symbolic Logic 49. 1 (1984): 231–233. DOI:

Angell, R., “A propositional logics with subjunctive conditionals”, Journal of Symbolic Logic 27, 3 (1962): 327–343. DOI:

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:

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:

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:

Kamide, N., and H. Wansing, “Symmetric and dual paraconsistent logics”, Logic and Logical Philosophy 19, 1–2 (2010): 7–30. DOI:

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

McCall, S., “Connexive implication”, Journal of Symbolic Logic 31 (1966): 415–433. DOI:

Nelson, D., “Constructible falsity”, Journal of Symbolic Logic 14, 1 (1949): 16–26. DOI:

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:

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.

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:

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:

Rauszer, C., “Applications of Kripke models to Heyting-Brouwer logic”, Studia Logica 36, 1–2 (1977): 61–71. DOI:

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:

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:

Wansing, H., “Falsification, natural deduction and bi-intuitionistic logic”, Journal of Logic and Computation 26, 1 (2016): 425–450. DOI:

Wansing, H., “Connexive logic”, Stanford Encyclopedia of Philosophy, 2014.

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.

ISSN: 1425-3305 (print version)

ISSN: 2300-9802 (electronic version)

Partnerzy platformy czasopism