Hans Tompits

From Łukasiewicz to Gentzen: On sequent-type refutation calculi for three-valued logics


While traditional proof calculi deal with the axiomatisation of the set of valid sentences of a given logic, refutation calculi, also referred to as complementary calculi, are concerned with axiomatising the invalid sentences, i.e., providing means to deduce invalid sentences from already established invalid ones. Albeit already Aristotle studied fallacies (i.e., invalid arguments) in his system of syllogisms, the first modern treatment of axiomatic rejection originates with Jan Łukasiewicz [7] and his study of expressing Aristotle’s syllogistic in modern logic [8, 9] where he introduced a Hilbert-type rejection system. This was continued by his student Jerzy Słupecki [16] and subsequently extended to a theory of rejected propositions [17, 21, 2, 18, 19]. [For a description of the development of this notion, cf., e.g., the paper by Wybraniec-Skardowska [22].] Furthermore, axiomatic rejection methods where not only studied for classical logic [13, 20] but also for varieties of logics, like intuitionistic logic [10, 4, 12], modal logics [5, 14], and others [1]. In this talk, I deal with the case of three-valued logics (and many-valued logics more generally), a logical approach again famously going back to Łukasiewicz [7]. While complete and uniform rejection methods were already quite extensively studied in the literature, like, e.g., in the works by Bryll and Maduch [3] and Skura [11], here I will discuss refutation calculi for such logics from the point of view of Gentzen-type systems. Furthermore, the relevance of the discussed calculi for nonmonotonic reasoning—notably for checking strong non-equivalence of logic programs under the answer-set semantics [6]—will be pointed out.

[1] Gerald Berger and Hans Tompits. On axiomatic rejection for the description logic ALC. In Michael Hanus and Ricardo Rocha, editors, Declarative Programming and Knowledge Management-Declarative Programming Days (KDPD 2013), Revised Selected Papers, volume 8439 of Lecture Notes in Computer Science, pages 65–82. Springer, 2014.
[2] Grzegorz Bryll. Kilka uzupelnień teorii zdań odrzuconych. Zeszyty Naukowe Wyższej Szkoły Pedagogigicznej w Opolu, Seria B, Studia i Monografie, 22:133–154, 1969.
[3] Grzegorz Bryll and Marian Maduch. Aksjomaty odrzucone dla wielowartościowych logik Łukasiewieza. Zeszyty Naukowe Wyższej Szkoły Pedagogicznej w Opolu, Matematyka, VI:3–19, 1969.
[4] Rafał Dutkiewicz. The method of axiomatic rejection for the intuitionistic propositional logic. Studia Logica, 48(4):449–459, 1989.
[5] Valentin Goranko. Refutation systems in modal logic. Studia Logica, 53(2):299–324, 1994.

[6] Vladimir Lifschitz, David Pearce, and Agustín Valverde. Strongly equivalent logic programs. ACM Transactions on Computational Logic, 2(4):526–541, 2001.
[7] Jan Łukasiewicz. Logika dwuwartościowa. Przegląd Filozoficzny, 23:189–205, 1921.
[8] Jan Łukasiewicz. O sylogistyce Arystotelesa. Akademii Umiejętności, 44, 1939.
Sprawozdania z Czynności i Posiedzeń Polskiej [9] Jan Łukasiewicz. Aristotle’s Syllogistic from the Standpoint of Modern Formal Logic. Clarendon Press, Oxford, 2nd edition, 1957.
[10] Tomasz Skura. A complete syntactic characterization of the intuitionistic logic. Reports on Mathematical Logic, 23, 1989.
[11] Tomasz Skura. Some results concerning refutation procedures. Acta Universitatis Wratislaviensis, Logika, 15, 1993.
[12] Tomasz Skura. Aspects of refutation procedures in the intuitionistic logic and related modal systems. Acta Universitatis Wratislaviensis, Logika, 20, 1999.
[13] Tomasz Skura. Refutation systems in propositional logic. In Handbook of Philosophical Logic, pages 115–157. Springer, 2011.
[14] Tomasz Skura. Refutation Methods in Modal Propositional Logic. Semper, Warszawa, 2013.
[15] Jerzy Słupecki. On Aristotelian syllogistic. Studia Philosophica, Posnaniae, 1951.
[16] Jerzy Słupecki. Z badań nad sylogistyk a ̨ Arystotelesa. Studia Philosophica, Posnaniae, Seria B,
6:5–30, 1951. English translation: [15].
[17] Jerzy Słupecki. Funkcja Łukasiewieza. Zeszyty Naukowe Uniwersytetu Wrocławskiego, Seria A, 3:33–40, 1959.
[18] Jerzy Słupecki, Grzegorz Bryll, and Urszula Wybraniec-Skardowska. Theory of rejected propositions I. Studia Logica, 29(1):75–115, 1971.
[19] Jerzy Słupecki, Grzegorz Bryll, and Urszula Wybraniec-Skardowska. Theory of rejected propositions II. Studia Logica, 30(1):97–139, 1972.
[20] M. Tiomkin. Proving unprovability. In Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988), pages 22–27. IEEE, 1988.
[21] Ursula Wybraniec-Skardowska. Teoria zdań odrzuconych. Zeszyty Naukowe Wyższej Szkoły Pedagogigicznej w Opolu, Seria B, Studia i Monografie, 22:5–131, 1969.
[22] Ursula Wybraniec-Skardowska. On the notion and function of the rejection of propositions. ActaUniversitatis Wratislaviensis, Logika, 23:179–202, 2005.