Assertional and Refutational Sequent-Type Calculi for Infectious Four-Valued Logics

Abstract

Um sowohl Inkonsistenz und Unbestimmheit logisch repräsentieren zu können, ist es nützlich, weitere Wahrheitswerte einzuführen.Für vierwertige Logiken kommt die Frage auf, wie die klassischen und zusätzlichen Wahrheitswerte miteinander agieren. Aus diesem Grund legen wir unseren Fokus auf sogenannte infektiöse vierwertige Logiken. Für infektiöse Logiken gilt, dass, wenn eine Komponente einer Formel einen infektiösen Wahrheitswert hat, die gesamte Formel diesen Wert zugewiesen bekommt.Um eine beweistheoretische Basis für die vierwertigen Logiken zu erstellen, untersuchen wir sowohl assertive als auch komplementäre Sequenzkalküle. Während assertive Kalküle die gültigen Formeln einer Logik axiomatisieren, axiomatisieren Komplementärkalküle ungültige Formeln und stellen daher eine rein syntaktische Methode dar um Ungültigkeit zu charakterisieren, ohne dass Gegenmodelle benötigt werden. Aus diesem Grund können Komplementärkalküle im automatischen Schließen und der Beweissuche hilfreich sein.In dieser Arbeit konstruieren wir systematisch assertive und komplementäre vierseitige und zweiseitige Sequenzkalküle für infektiöse vierwertige Logiken.

To represent both inconsistency and indeterminateness when formalising statements, it is useful to introduce additional truth values. In this four-valued setting, the question arises how the classical and the added truth values interact with each other. Hence, we focus on so-called infectious four-valued logics. For infectious logics, it holds that, if a component of a sentence has the infectious truth value, the entire sentence gets this truth value assigned. To provide a proof-theoretic basis for the four-valued infectious logics, we study both assertional and refutational sequent-style calculi. While assertional calculi axiomatise the valid formulae of a logic, refutational calculi, or refutation systems, are proof systems for axiomatising invalid formulae and provide a purely syntactic method for rejecting formulae without having to consider countermodels. Therefore, refutation systems can be useful for automated deduction and proof search.In this thesis, we systematically construct assertional and refutational sequent-style calculi for infectious four-valued logics, both in a four-sided, as well as two-sided setting.