On the axiomatisation of non-validity: Sequent-type rejection systems and beyond

Abstract

Ein Verwerfungskalkül ist ein formales Beweissystem zur axiomatischen Charakterisierung einer bestimmten Klasse von ungültigen Formeln einer Logik. Im Gegensatz zu traditioneller Beweistheorie, deren Ziel es ist, die Übertragung von Gültigkeit zu formalisieren, dienen Verwerfungskalküle dem rein syntaktischen Erhalt von Ungültigkeiten. Derartige Kalküle finden ihren Ursprung bei Jan Łukasiewicz und wurden seither, bisweilen auch unabhängig, für unterschiedliche Logiken entwickelt. In dieser Arbeit legen wir eine umfangreiche Darstellung des gegenwärtigen Forschungsstandes zu Verwerfungskalkülen dar und beschreiben die historische wie auch konzeptuelle Entwicklung der axiomatischen Verwerfung. Dabei legen wir besonderes Augenmerk auf jene Verwerfungskalküle, die in Form eines Sequenzenkalküls formalisiert sind. Desweiteren stellen wir auch unteschiedliche neue Resultate vor. Einerseits generalisieren wir Verwerfungssysteme auf Basis zweiseitiger Sequenzenkalküle, welche von Oetsch und Tompits für gewisse dreiwertige Logiken entwickelt wurden, auf den vierwertigen Fall. Andererseits motivieren und skizzieren wir zwei neuartige Möglichkeiten der axiomatischen Charakterisierung bestimmter Klassen von Logiken ausgehend von der sogenannten ``biaspektuellen Charakterisierung von Logiken ́ ́ nach Łukasiewicz. Schlußendlich erkunden und erörtern wir neue Richtungen zur axiomatischen Verwerfung jenseits des Bereichs der formalen Logik, basierend auf Ideen aus der Sprechakttheorie, der beweistheoretischen Semantik sowie der metaphysischen Begründung.

A rejection system is a proof calculus axiomatically characterising some class of non-valid formulas of a logic. In contrast to the usual traditions of formalising the propagation of validity, rejection systems preserve, in a purely syntactic manner, the non-validities of a logic. Such systems were pioneered by Jan Łukasiewicz and subsequently, and occasionally independently, proposed for a multitude of logics. In this thesis, we provide a comprehensive exposition on the current research on rejection systems, as well as a thorough account of the historical and conceptional development of axiomatic rejection. In doing so, a particular emphasis will be on rejection systems formulated in terms of a sequent-type calculus. As part of our endeavour, we also provide new results, extending previous work by Oetsch and Tompits on two-sided sequent-type rejection systems for three-valued logics to the four-valued case. Additionally, we motivate and sketch two novel takes on possible axiomatic characterisations for certain classes of logics, framed against the so-called ``bi-aspectual characterisation of logic ́ ́, as championed by Łukasiewicz. Finally, we explore and discuss new directions for axiomatic rejection research beyond the purview of formal logic, dealing with ideas from speech-act theory, proof-theoretic semantics, and metaphysical grounding.