Uniform Cut-Free Bisequent Calculi for Three-Valued Logics

Andrzej Indrzejczak; Yaroslav Petrukhin

doi:10.12775/LLP.2024.019

Authors

Andrzej Indrzejczak Department of Logic, Institute of Philosophy, University of Łódź https://orcid.org/0000-0003-4063-1651
Yaroslav Petrukhin Center for Philosophy of Naturey, University of Łódź https://orcid.org/0000-0002-7731-1339

DOI:

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

Keywords

bisequent calculus, cut elimination, many-valued logic, three-valued logic, interpolation theorem

Abstract

We present a uniform characterisation of three-valued logics by means of a bisequent calculus (BSC). It is a generalised form of a sequent calculus (SC) where rules operate on the ordered pairs of ordinary sequents. BSC may be treated as the weakest kind of system in the rich family of generalised SC operating on items being some collections of ordinary sequents, like hypersequent and nested sequent calculi. It seems that for many non-classical logics, including some many-valued, paraconsistent and modal logics, the reasonably modest generalisation of standard SC offered by BSC is sufficient. In this paper, we examine a variety of three-valued logics and show how they can be formalised in the framework of BSC. We present a constructive syntactic proof that these systems are cut-free, satisfy the subformula property, and allow one to prove the interpolation theorem in many cases.

References

Anderson, A. R., Belnap, N. D., Entailment. The Logic of Relevance and Necessity, Vol. 1, Princeton, NJ: Princeton University Press, 1975.

Asenjo, F. G., “A calculus of antinomies”, Notre Dame Journal of Formal Logic, 7, 1 (1966): 103–105. DOI: https://doi.org/10.1305/ndjfl/1093958482

Asenjo, F. G., and J. Tamburino, “Logic of antinomies”, Notre Dame Journal of Formal Logic, 16, 1 (1975): 17–44. DOI: https://doi.org/10.1305/ndjfl/1093891610

Avron, A., “On an implicational connective of RM”, Notre Dame Journal of Formal Logic, 27, 2 (1986): 201–209. DOI: https://doi.org/10.1305/ndjfl/1093636612

Avron, A., “Natural 3-valued logics – characterization and proof theory”, The Journal of Symbolic Logic, 61, 1 (1991): 276–294. DOI: https://doi.org/10.2307/2274919

Avron, A., J. Ben-Naim, and B. Konikowska, “Cut-free ordinary sequent calculi for logics having generalized finite-valued semantics”, Logica Universalis 1, 1, (2007): 41–70. DOI: https://doi.org/10.1007/s11787-006-0003-6

Baaz, M., C. G. Fermüller, and G. Salzer, “Automated deduction for many-valued logic”, pages 1355–1402 in A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, vol. 2, Elsevier, Amsterdam, 2001.

Baaz, M., C. G. Fermüller, R. Zach, “Elimination of cuts in first-order finite-valued logics”, Journal of Information Processing and Cybernetics, 29, 6 (1994): 333–355.

Batens, D., “Paraconsistent extensional propositional logics”, Logique et Analyse, 23, 90–91 (1980): 195–234.

Belnap, N. D., “A useful four-valued logic”, pages 7–37 in J. M. Dunn and G. Epstein (eds.), Modern Uses of Multiple-Valued Logic, Boston: Reidel Publishing Company, 1977. DOI: https://doi.org/10.1007/978-94-010-1161-7_2

Belnap, N. D., “How a computer should think”, pages 30–56 in G. Rule (ed.), Contemporary Aspects of Philosophy, Oriel Press Ltd., 1977.

Bochman, A., “Biconsequence relations: A four-valued formalism of reasoning with inconsistency and incompleteness”, Notre Dame Journal of Formal Logic, 39, 1 (1998): 47–73. DOI: https://doi.org/10.1305/ndjfl/1039293020

Bochvar, D. A., “On a three-valued logical calculus and its application to the analysis of the paradoxes of the classical extended functional calculus”, History and Philosophy of Logic 2, 1–2 (1981): 87–112. English translation of Bochvar’s paper of 1938. DOI: https://doi.org/10.1080/01445348108837023

Carnielli, W. A., J. Marcos, “Taxonomy of C-systems”, pages 1–94 in W. A. Carnielli, M. E. Coniglio and I. M. L. D’Ottaviano (eds.), Paraconsistency: The Logical Way to the Inconsistent, CRC Press, 2002.

da Costa N. C. A., “On the theory of inconsistent formal systems”, Notre Dame Journal of Formal Logic, 15, 4 (1974): 497–510. DOI: https://doi.org/10.1305/ndjfl/1093891487

D’Ottaviano, I. M. L., N. C. A. da Costa, “Sur un probléme de Jaśkowski”, Comptes Rendus Acad. Sci. Paris 270A (1970): 1349–1353.

Doherty, P., “A constraint-based approach to proof-procedures for multi-valued logics”, Proceedings of the 1st World Conference on Fundamentals of Artificial Intelligence, Berlin, Heidelberg, Germany: Springer, 1991.

Dragalin, A. G., Mathematical Intuitionism. Introduction to Proof Theory, Providence: American Mathematical Society, 1988.

Dunn, J. M., “Intuitive semantics for first-degree entailment and coupled trees”, Philosophical Studies, 29, 3 (1976): 149–168. DOI: https://doi.org/10.1007/BF00373152

Fitting, M., “Kleene’s three valued logics and their children”, Fundamenta Informaticae, 20, 1 (1994): 113–131. DOI: https://doi.org/10.3233/FI-1994-201234

Fjellstad, A., “Non-classical elegance for sequent calculus enthusiasts”, Studia Logica, 105, 1 (2017): 93–119. DOI: https://doi.org/10.1007/s11225-016-9683-y

Fjellstad, A., “Structural proof theory for first-order weak Kleene logics”, Journal of Applied Non-Classical Logics, 30, 3 (2020): 272–289. DOI: https://doi.org/10.1080/11663081.2020.1782593

Gödel, K., “Zum intuitionistischen Aussgenkalkül”, Anz. Akad. Wiss. Wien, 69 (1932): 65–66.

Hähnle, R., Automated Deduction in Multiple-Valued Logics, Oxford University Press, 1994.

Hähnle, R., “Tableaux and related methods”, pages 101–177 in A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, Elsevier, Amsterdam, 2001. DOI: https://doi.org/10.1016/B978-044450813-3/50005-9

Halldén, S., The Logic of Nonsense, Lundequista Bokhandeln, Uppsala, 1949.

Heyting, A., “Die Formalen Regeln der intuitionistischen Logik. Sitzungsber”, Preussischen Acad. Wiss. Berlin, (1930): 42–46.

Indrzejczak, A., “Two is enough – bisequent calculus for S5”, pages 277–294 in A. Herzig and A. Popescu (eds.), Frontiers of Combining Systems. 12th International Symposium, FroCoS 2019, Cham: Springer Nature, 2019. DOI: https://doi.org/10.1007/978-3-030-29007-8_16

Indrzejczak, A., “Free definite description theory – sequent calculi and cut elimination”, Logic and Logical Philosophy 29, 4 (2020): 505–539. DOI: https://doi.org/10.12775/LLP.2020.020

Indrzejczak, A., Sequents and Trees. An Introduction to the Theory and Applications of Propositional Sequent Calculi, Birkhäuser, 2021. DOI: https://doi.org/10.1007/978-3-030-57145-0

Indrzejczak, A., “Russellian definite description theory – a proof-theoretic approach”, The Review of Symbolic Logic. 16, 2 (2023): 624–649. DOI: https://doi.org/10.1017/S1755020321000289

Indrzejczak, A.: “Bisequent calculus for four-valued quasi-relevant logics: Cut elimination and interpolation”. Journal of Automated Reasoning, 67, 37 (2023): 1–19. DOI: https://doi.org/10.1007/s10817-023-09685-z

Indrzejczak, A., and Y. Petrukhin, “A uniform formalisation of three-valued logics in bisequent calculus”, pages 325–343 in B. Pientka and C. Tinelli (eds.), International Conference on Automated Deduction, CADE 2023: Automated Deduction – CADE 29, Springer (2023). DOI: https://doi.org/10.1007/978-3-031-38499-8_19

Indrzejczak, A., and Y. Petrukhin, “Bisequent calculi for neutral free logic with definite descriptions”, accepted to ARQNL2024.

Indrzejczak, A., and M. Zawidzki, “Tableaux for free logics with descriptions”, pp. 56–73 in A. Das, S. Negri (eds.), Automated Reasoning with Analytic Tableaux and Related Methods, Springer, Berlin–Heidelberg, 2021.

Jaśkowski, S., “Recherches sur le système de la logique intuitioniste”, Actes Congr. Int. phil. sci., 6 (1936): 58–61.

Jaśkowski, S., “Rachunek zdań dla systemów dedukcyjnych sprzecznych”, Studia Societatis Scientiarum Torunensis, Sectio A, Vol. I, No. 5, Toruń, 57–77, 1948. English translation: “A propositional calculus for inconsistent deductive systems”, Logic and Logical Philosophy, 7 (1999): 35–56. DOI: https://doi.org/10.12775/LLP.1999.003

Kleene, S. C., “On a notation for ordinal numbers”, The Journal of Symbolic Logic 3, 1 (1938): 150–155. DOI: https://doi.org/10.2307/2267778

Komendantskaya, E. Y., “Functional expressibility of regular Kleene’s logics” (in Russian), Logical Investigations. 15, (2009): 116–128.

Lehmann, S., “Strict Fregean free logic”, Journal of Philosophical Logic, 23, 3, (1994): 307–336. DOI: https://doi.org/10.1007/BF01048484

Lellmann, B., and F. Poggiolesi, “Nested sequent or tree-hypersequents: A survey”, in R. Padro and Y. Weiss (eds.), Saul Kripke on Modal logic, In press. https://hal.science/hal-03590537/document

Łukasiewicz, J., “On three-valued logic”, pages 87–88 in L. Borkowski (ed.), Jan Łukasiewicz: Selected Works, Amsterdam, North-Holland Publishing Company, 1970. English translation of Łukasiewicz’s paper of 1920.

Marcos, J., “On a problem of da Costa”, pages 53–69 in G. Sica (ed.) Essays of the Foundations of Mathematics and Logic, vol. 2, Polimetrica, 2005.

McCarty, J., “A basis for a mathematical theory of computation”, Studies in Logic and the Foundations of Mathematics, 35 (1963): 33–70. DOI: https://doi.org/10.1016/S0049-237X(08)72018-4

Metcalfe, G., N. Olivetti, and D. Gabbay, Proof Theory for Fuzzy Logics, Cham: Springer, 2008. DOI: https://doi.org/10.1007/978-1-4020-9409-5

Negri, S., and J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge, 2001. DOI: https://doi.org/10.1017/CBO9780511527340

Osorio, M., and J. L. Carballido, “Brief study of G′ 3 logic”, Journal of Applied Non-Classical Logic, 18, 4 (2008): 475–499. DOI: https://doi.org/10.3166/jancl.18.475-499

Pałasińska, K., “Three-element nonfinitely axiomatizable matrices”, Studia Logica, 53 (1994): 361–372. DOI: https://doi.org/10.1007/BF01057933

Paoli, F., and M. Pra Baldi, “Proof theory of Paraconsistent Weak Kleene Logic”, Studia Logica, 108, 4 (2020): 779–802. DOI: https://doi.org/10.1007/s11225-019-09876-z

Pavlović, E., and N. Gratzl, “Neutral free logic: motivation, proof theory and models”, Journal of Philosophical Logic, 52 (2021): 519–554. DOI: https://doi.org/10.1007/s10992-022-09679-z

Petrukhin, Y., “Natural deduction for Post’s logics and their duals”, Logica Universalis, 12, 1–2, (2018): 83–100. DOI: https://doi.org/10.1007/s11787-018-0190-y

Poggiolesi, F., Gentzen Calculi for Modal Propositional Logic, Springer, 2010. DOI: https://doi.org/10.1007/978-90-481-9670-8

Post, E., “Introduction to a general theory of elementary propositions”, American Journals of Mathematics, 43, (1921): 163–185. DOI: https://doi.org/10.2307/2370324

Priest, G., “The logic of paradox”, Journal of Philosophical Logic 8 (1979): 219–241. DOI: https://doi.org/10.1007/BF00258428

Priest, G.: “Paraconsistent logic”, pages 287–393 in D. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, 2nd edition, vol. 6, Kluwer Academic Publishers, 2002. DOI: https://doi.org/10.1007/978-94-017-0460-1_4

Rescher, N., Many-Valued Logic, New York, McGraw Hill, 1969.

Rozonoer, L., “On interpretation of inconsistent theories”, Information Sciences 47, 3, (1989): 243–266. DOI: https://doi.org/10.1016/0020-0255(89)90003-0

Sette, A. M., “On propositional calculus P1”, Mathematica Japonica, 18, 3 (1973): 173–180.

Sette, A. M., and W. A. Carnieli, “Maximal weakly-intuitionistic logics”, Studia Logica, 55, 1 (1995): 181–203. DOI: https://doi.org/10.1007/BF01053037

Słupecki, J., “Proof of axiomatizability of full many-valued systems of calculus of propositions”, Studia Logica, 29, (1971): 155–168. [English translation of the paper by 1939]. DOI: https://doi.org/10.1007/BF02121872

Słupecki E., J. Bryll, and T. Prucnal, “Some remarks on the three-valued logic of J. Łukasiewicz”, Studia Logica, 21 (1967): 45–70. DOI: https://doi.org/10.1007/BF02123418

Sobociński, B., “Axiomatization of certain many-valued systems of the theory of deduction”, Roczniki Prac Naukowych Zrzeszenia Asystentów Uniwersytetu Józefa Piłsudskiego w Warszawie, 1 (1936): 399–419.

Sobociński, B., “Axiomatization of a partial system of three-valued calculus of propositions”, The Journal of Computing Systems, 1 (1952): 23–55.

Stenlund, S., “The Logic of description and existence”, Filosofiska Studier no 18, Uppsala, 1973.

Suszko R.: “The Fregean axiom and Polish mathematical logic in the 1920’s”, Studia Logica, 36, (1977): 373–380. DOI: https://doi.org/10.1007/BF02120672

Tomova, N. E., “A lattice of implicative extensions of regular Kleene’s logics”, Reports on Mathematical Logic, 47, (2012): 173–182. DOI: https://doi.org/10.4467/20842589RM.12.008.0689

Troelstra, A. S., and H. Schwichtenberg, Basic Proof Theory, Oxford, Oxford University Press, 1996. DOI: https://doi.org/10.1017/CBO9781139168717

Wansing, H., “Sequent systems for modal logic”, pages 61-145 in D. M. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, vol 8, Dordrecht, Kluwer, 2002. DOI: https://doi.org/10.1007/978-94-010-0387-2_2

Wintein, S., and R. Muskens, “Interpolation methods for Dunn logics and their extensions”, Studia Logica, 105, 6 (2017): 1319–1348. DOI: https://doi.org/10.1007/s11225-017-9720-5