Normalisation for Some Quite Interesting Many-Valued Logics

Nils Kürbis, Yaroslav Petrukhin



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 RM3 and RM3. Also, we present a detailed version of Prawitz’s proof of Nelson’s logic N4 and its extension by intuitionist negation.


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

Full Text:



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

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:

Asenjo, F., and J. Tamburino (1975), “Logic of antinomies”, Notre Dame Journal of Formal Logic 61 (2): 17–44. DOI:

Avron, A. (1986), “On an implication connective of RM”, Notre Dame Journal of Formal Logic 27 (2): 201–209. DOI:

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

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:

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:

Bolotov, A., and V. Shangin (2012), “Natural deduction system in paraconsistent setting: Proof search for PCont”, Journal of Intelligent Systems 21: 1–24. DOI:

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:

Dunn, J. (2000), “Partiality and its dual”, Studia Logica 66: 5–40. DOI:

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

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:

Kamide, N., and H. Wansing (2015), Proof Theory of N4-related Paraconsistent Logics, Milton Keynes: College Publications. DOI:

Kaminski, M., and N. Francez (2021), “Calculi for many-valued logics”, Logica Universalis 15: 193–226. DOI:

Kleene, S. (1938), “On a notation for ordinal numbers”, Journal of Symbolic Logic 3: 150–155. DOI:

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:

Kürbis, N. (2015), “What is wrong with classical negation?”, Grazer Philosophische Studien 92 (1): 51–85. DOI:

Kürbis, N. (2019), Proof and Falsity. A Logical Investigation, Cambridge University Press. DOI:

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

Omori, H., and H. Wansing (2017), “40 years of fde: An introductory overview”, Studia Logica 105: 1021–1049. DOI:

Petrukhin, Y. (2018), “Generalized correspondence analysis for three-valued logics” Logica Universalis 12: 432–460. DOI:

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:

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:

Petrukhin, Y., and V. Shangin (2020), “Correspondence analysis and automated proof-searching for first degree entailment”, European Journal of Mathematics 6: 1452–1495. DOI:

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:

Priest, G. (2002), “Paraconsistent logic”, pages 287–393 in Handbook of Philosophical Logic, vol. 6, Kluwer Academic Publishers. DOI:

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:

Rozonoer, L. (1989), “On interpretation of inconsistent theories”, Information Sciences 47: 243–266. DOI:

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:

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:

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:

Tennat, N. (2019), “GP’s LP”, pages 481–506 in Graham Priest on Dialetheism and Paraconsistency, Springer. DOI:

Troestra, A., and H. Schwichtenberg (2000), Basic Proof Theory, 2ed, Cambridge University Press. DOI:

Wansing, H. (2001), “Negation”, in L. Goble (Ed.), The Blackwell Guide to Philosophical Logic, Oxford: Blackwell. DOI:

Zimmermann, E. (2002), “Peirce’s rule in natural deduction”, Theoretical Computer Science 275: 561–574. DOI:

ISSN: 1425-3305 (print version)

ISSN: 2300-9802 (electronic version)

Partnerzy platformy czasopism