Normalisation for Some Quite Interesting Many-Valued Logics

Nils Kürbis; Yaroslav Petrukhin

doi:10.12775/LLP.2021.009

Authors

Nils Kürbis Department of Logic, Institute of Philosophy, University of Lódź
Yaroslav Petrukhin Department of Logic, Institute of Philosophy, University of Lódź

DOI:

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

Keywords

natural deduction, normalisation, three-valued logic, four-valued logic, logic of paradox, Nelson logic

Abstract

In this paper, we consider a set of quite interesting three- and four-valued logics and prove the normalisation theorem for their natural deduction formulations. Among the logics in question are the Logic of Paradox, First Degree Entailment, Strong Kleene logic, and some of their implicative extensions, including RM₃ and RM₃^⊃. Also, we present a detailed version of Prawitz’s proof of Nelson’s logic N4 and its extension by intuitionist negation.

References

Almukdad, A., and D. Nelson (1984), “Constructible falsity and inexact predicates”, Journal of Symbolic Logic 49: 231–233. DOI: http://dx.doi.org/10.2307/2274105

Anderson, A., and N. Belnap (1975), Entailment. The Logic of Relevance and Necessity, Vol. I, Princeton University Press.

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

Asenjo, F., and J. Tamburino (1975), “Logic of antinomies”, Notre Dame Journal of Formal Logic 61 (2): 17–44. DOI: http://dx.doi.org/10.1305/ndjfl/1093891610

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

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

Baaz, M., C. Fermüller, and R. Zach (1993a), “Dual systems of sequents and tableaux for many-valued logics”, Bulletin of the EATCS 51: 192–197.

Baaz, M., C. Fermüller, and R. Zach (1993b), “Systematic construction of natural deduction systems for many-valued logics”, pages 208–213 in Pros. 23rd International Symposium on Multiple Valued Logic, IEEE Press. DOI: http://dx.doi.org/10.1109/ISMVL.1993.289558

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

Belnap, N. (1977), “A useful four-valued logic”, pages 7–37 in Modern Uses of Multiple-Valued Logic, Kluwer Academic Publishers. DOI: http://dx.doi.org/10.1007/978-94-010-1161-7_2

Bolotov, A., and V. Shangin (2012), “Natural deduction system in paraconsistent setting: Proof search for PCont”, Journal of Intelligent Systems 21: 1–24. DOI: http://dx.doi.org/10.1515/jisys-2011-0021

Brady, R. (1982), “Completeness proofs for the systems RM3 and BN4”, Logique et Analyse 25: 51–61.

D’Ottaviano, I., and N. da Costa (1970), “Sur un probléme de Jaśkowski”, Comptes Rendus de l’Académie des Sciences de Paris 270: 1349–1353.

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

Dunn, J. (2000), “Partiality and its dual”, Studia Logica 66: 5–40. DOI: http://dx.doi.org/10.1023/A:1026740726955

Englander, C., E. Haeusler, and L. Pereira (2014), “Finitely many-valued logics and natural deduction”, Logic journal of the IGPL 22: 333–354. DOI: http://dx.doi.org/10.1093/jigpal/jzt032

Jaśkowski, S. (1948), “Rachunek zdań dla systemów dedukcyjnych sprzecznycìh”, Studia Societatis Scientiarum Torunensis, Sectio A vol. I (5): 57–77.

Jaśkowski, S. (1999), “A propositional calculus for inconsistent deductive systems”, Logic and Logical Philosophy 7: 35–56. English translation of Polish paper (Jaśkowski, 1948). DOI: http://dx.doi.org/10.12775/LLP.1999.003

Kamide, N., and H. Wansing (2015), Proof Theory of N4-related Paraconsistent Logics, Milton Keynes: College Publications. DOI: http://dx.doi.org/10.1007/s11225-017-9729-9

Kaminski, M., and N. Francez (2021), “Calculi for many-valued logics”, Logica Universalis 15: 193–226. DOI: http://dx.doi.org/10.1007/s11787-021-00274-5

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

Kooi, B. and A. Tamminga (2012), “Completeness via correspondence for extensions of the logic of paradox”, The Review of Symbolic Logic 5: 720–730. DOI: http://dx.doi.org/10.1017/S1755020312000196

Kürbis, N. (2015), “What is wrong with classical negation?”, Grazer Philosophische Studien 92 (1): 51–85. DOI: http://dx.doi.org/10.1163/9789004310841_004

Kürbis, N. (2019), Proof and Falsity. A Logical Investigation, Cambridge University Press. DOI: http://dx.doi.org/10.1017/9781108686792

Łukasiewicz, J. (1920), “O logice trójwartościowej”, Ruch Filozoficzny 5: 170–171.

Łukasiewicz, J. (1941), “Die Logik und das Grundlagenproblem” Les Entretiens de Zürich sur les fondements et la méthode das sciences mathématiques 12: 6–9.

Łukasiewicz, J. (1970), Selected Works, L. Borkowski (Ed.), North-Holland & PWN.

Nelson, D. (1949), “Constructible falsity”, Journal of Symbolic Logic 14: 16–26. DOI: http://dx.doi.org/10.2307/2268973

Omori, H., and H. Wansing (2017), “40 years of fde: An introductory overview”, Studia Logica 105: 1021–1049. DOI: http://dx.doi.org/10.1007/s11225-017-9748-6

Petrukhin, Y. (2018), “Generalized correspondence analysis for three-valued logics” Logica Universalis 12: 432–460. DOI: http://dx.doi.org/10.1007/s11787-018-0212-9

Petrukhin, Y., and V. Shangin (2017), “Automated correspondence analysis for the binary extensions of the logic of paradox”, The Review of Symbolic Logic 10: 756–781. DOI: http://dx.doi.org/10.1017/S1755020317000156

Petrukhin, Y., and V. Shangin (2019), “Automated proof-searching for strong Kleene logic and its binary extensions via correspondence analysis”, Logic and Logical Philosophy 28 (2): 223–257. DOI: http://dx.doi.org/10.12775/LLP.2018.009

Petrukhin, Y., and V. Shangin (2020), “Correspondence analysis and automated proof-searching for first degree entailment”, European Journal of Mathematics 6: 1452–1495. DOI: http://dx.doi.org/10.1007/s40879-019-00344-5

Popov, V. (1989), “Sequent formulations of paraconsistent logical systems” (in russian), pages 285–289 in Semantic and Syntactic Investigations of Non-Extensional Logics, Nauka.

Popov, V. (2009), “Between the logic par and the set of all formulas” (in russian), pages 93–95 in The Proceeding of the Sixth Smirnov Readings in Logic, Contemporary Notebooks.

Prawitz, D. (1965), Natural Deduction, Stockholm, Göteborg, Uppsala: Almqvist and Wiksell.

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

Priest, G. (2002), “Paraconsistent logic”, pages 287–393 in Handbook of Philosophical Logic, vol. 6, Kluwer Academic Publishers. DOI: http://dx.doi.org/10.1007/978-94-017-0460-1_4

Pynko, A. (1999), “Functional completeness and axiomatizability within Belnap’s four-valued logic and and its expansion”, Journal of Applied Non-Classical Logics 9: 61–105. DOI: http://dx.doi.org/10.1080/11663081.1999.10510958

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

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

Słupecki, J. (1939), “Dowód aksjomatyzowalności pelnych systemów wielowartościowych rachunku zdań”, Comptes Rendus des Seances de la Sociéte des Sciences et des Lettres de Varsovie XXXII, Classe III (1–3): 110–128.

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

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

Tamminga, A. (2014), “Correspondence analysis for strong three-valued logic”, Logical Investigations 20: 255–268. DOI: http://dx.doi.org/10.21146/2074-1472-2014-20-0-253-266

Tennat, N. (2019), “GP’s LP”, pages 481–506 in Graham Priest on Dialetheism and Paraconsistency, Springer. DOI: http://dx.doi.org/10.1007/978-3-030-25365-3_23

Troestra, A., and H. Schwichtenberg (2000), Basic Proof Theory, 2ed, Cambridge University Press. DOI: http://dx.doi.org/10.1017/CBO9781139168717

Wansing, H. (2001), “Negation”, in L. Goble (Ed.), The Blackwell Guide to Philosophical Logic, Oxford: Blackwell. DOI: http://dx.doi.org/10.1002/9781405164801.ch18

Zimmermann, E. (2002), “Peirce’s rule in natural deduction”, Theoretical Computer Science 275: 561–574. DOI: http://dx.doi.org/10.1016/S0304-3975(01)00296-1