
Proof Theory of N4-Paraconsistent Logics
Das vorliegende Buch ist die erste Monographie überhaupt, die sich schwerpunktmäßig mit der Beweistheorie parakonsistenter Logiken in der Nähe der vierwertigen, konstruktiven parakonsistenten Logik N4 von David Nelson beschäftigt. Der Band versammelt eine Reihe von Arbeiten, die die Autoren einzeln oder gemeinsam zu verschiedenen Systemen der inkonsistenztoleranten Logik geschrieben haben.
Das Material deckt die strukturelle Beweistheorie von - N4, - seinen Fragmenten, einschließlich der Logik ersten Grades, - verwandten Logiken, wie Dreigitterlogiken, konnektiven Systemen, Systemen der symmetrischen und dualen parakonsistenten Logik und Variationen der bi-intuitionistischen Logik, - parakonsistenten temporalen Logiken, - substrukturellen Subsystemen von N4, wie parakonsistenten intuitionistischen linearen Logiken, parakonsistenten Logiken basierend auf involutiven Quantalen und parakonsistenten Lambek-Logiken. Obwohl die Beweistheorie von N4 und N4-verwandten Logiken das zentrale Thema der vorliegenden Monographie ist, spielen auch Modelle und modelltheoretische Semantiken eine wichtige Rolle in der Darstellung. Die behandelten relationalen Modelle im Kripke-Stil bieten einen motivierenden und intuitiv ansprechenden Einblick in die Logiken, in Bezug auf die sie sich als solide und vollständig erweisen.
Nichtsdestotrotz liegt der Schwerpunkt auf Beweissystemen im Gentzen-Stil - insbesondere Sequentenkalkülen der Standard- und weniger standardisierten Art - für parakonsistente Logiken, und die Schnitteliminierung und ihre Konsequenzen sind ein zentrales Thema. Ein verbindendes Element der Darstellung ist die wiederholte Anwendung von Einbettungstheoremen, um Ergebnisse aus anderen Logiken wie der intuitionistischen Logik auf den parakonsistenten Fall zu übertragen.