On constructing assertional and complementary sequent calculi for non-deterministic finite-valued logics

Abstract

Nichtdeterministische endlichwertige Logiken, eingeführt von Avron und Lev, sind eine Verallgemeinerung von klassischen endlichwertigen Logiken in der die Auswertung von Formeln im Allgemeinen eine nicht-funktionale Relation darstellt. In dieser Arbeit führen wir systematische Methoden zur Konstruktion von sowohl assertiven als auch komplementären Sequenzenkalkülen für jede gegebene nichtdeterministische endlichwertige Logik ein. Im Gegensatz zu traditionellen Kalkülen, welche die gültigen Formeln einer Logik axiomatisieren, formalisieren komplementäre Kalküle die ungültigen Formeln einer Logik. Somit erlauben komplementäre Kalküle eine rein syntaktische Charakterisierung von Ungültigkeit ohne die Notwendigkeit der Verwendung von Gegenmodellen, was besonders im Bereich des automatischen Schließens von Vorteil sein kann. Die ersten komplementären Kalküle wurden von Jan Łukasiewicz in den 1930er Jahren eingeführt und in weiterer Folge wurden zahlreiche andere Kalküle dieser Art für unterschiedliche bekannte Logiken entwickelt. Unsere eingeführten Methoden basieren auf sogenannten mehrseitigen Sequenten, welche eine natürliche Verallgemeinerung von klassischen zweiseitigen Sequenten für mehrwertige Logiken darstellen. Weiters sind die systematischen Konstruktionen, die in dieser Arbeit eingeführt werden, Verallgemeinerungen von existierenden analogen Methoden für traditionelle mehrwertige Logiken, und zwar der Konstruktionen von Zach für den assertiven Fall und von Bogojeski und Tompits für den Komplementären. Desweiteren führen wir durch Anwendung unserer Methode konkrete Kalküle für ausgewählte parakonsistente Logiken ein, welche in eleganter Weise durch nichtdeterministische zwei- und dreiwertige Semantiken charakterisiert werden können.

Non-deterministic finite-valued logics, proposed by Avron and Lev, are a generalisation of traditional finite-valued logics where the evaluation of formulas represents in general a non-functional relation. In this thesis, we introduce systematic methods for constructing both assertional as well as complementary sequent-style proof systems for any given non-deterministic finite-valued logic. In contrast to traditional, assertional proof systems, whose aim are to axiomatise the valid formulas of a logic, a complementary system, also referred to as a rejection system, is a proof system which axiomatises the invalid formulasof a logic. Rejection systems therefore introduce a purely syntactic way of determining non-validity without having to consider countermodels, which can be useful in procedures for automated deduction and proof search. The method of axiomatic rejection was first introduced by Jan Łukasiewicz in the 1930s and subsequently rejection systems for many well-known logics have been proposed. Our method is based on so-called many-sided sequents, which are a natural generalisation of standard two-sided sequents to the finite-valued case. Furthermore, the systematic constructions we introduce in this thesis are generalisations of similar methods for standard finite-valued logics as proposed by Zach for assertional sequent-type calculi and by Bogojeski and Tompits for the complementary case. As special instances of our method, we provide concrete calculi for specific paraconsistent logics which can be elegantly expressed in terms of non-deterministic two- and three-valued semantics, respectively.