Beweistheorie für nicht-lineare Quantoren: CERES et. al.

Die Quantoren Für alle und Es gibt gehören zu den wichtigsten Bestandteile der Prädikatenlogik erster Ordnung. Sie ermöglichen es aber nicht wechselseitige Abhängigkeiten auszudrücken, wie Für alle x gibt es ein u, unabhängig von y, und für alle y gibt es ein v unabhängig von x. Das ist Aufgabe der von Leon Henkin eingeführten und nach ihm benannten Quantoren und nicht linearen Quantoren im Allgemeinen. Es stellte sich heraus, dass die Prädikatenlogik erster Stufe, erweitert durch Henkin-Quantoren, unvollständig ist. Das bedeutet, dass (wie in der Logik zweiter Ordnung) kein Axiom- und Regelsystem existiert in welchem alle wahren Sätze ableitbar sind. Das vorliegende Projekt beschäftigt sich mit der Erstellung von Herleitungssystemen, die zumindest den Beweis der wichtigsten natürlichen Sätze mit nicht linearen Quantoren erlauben, sowie mit der beweistheoretischen Analyse dieser Herleitungssysteme. Für die Systeme sollen dabei insbesondere der Schnitteliminationssatz und Varianten des Satzes von Herbrand gezeigt werden. Die Möglichkeit Schnitte zu eliminieren ist wesentlich für die Analyse von Beweisen erster Ordnung (Proof Mining). Bei der Analyse von Beweisen ist an Herleitungen mit strukturierten Objekten, wie Vektoren, zu denken, die mit Hilfe von nicht linearen Quantoren direkt und ohne Referenz auf eine Kodierung wie Paarbildung und Projektion dargestellt werden können. Das erlaubt zum Beispiel die Analyse von Beweisen in der affinen Geometrie. Die Ergebnisse des Projektes sollen die Erweiterung von CERES auf Logik erster Ordnung mit nicht linearen Quantoren ermöglichen (CERES ist das zurzeit effizienteste Schnitteliminationssystem). Nach Barwise sind nicht lineare Quantoren notwendig um bestimmte sprachliche Kontexte adäquat darzustellen. Mit Hilfe dieses Projektes soll der Umgang mit sprachlichen Kontexten automatisiert werden. Das dient unter anderem der Unterstützung der automatischen Analyse linguistischer Argumentationsformend.

Die Quantoren (für alle) und (es gibt) gehören zu den wichtigsten Bestandteile der Prädikatenlogik erster Ordnung. Sie ermöglichen es aber nicht wechselseitige Abhängigkeiten auzudrücken, wie für alle x gibt es ein u, unabhängig von y, und für alle y gibt es ein v unabhängig von x. Das ist Aufgabe der von Leon Henkin eingeführten und nach ihm benannten Quantoren und nicht linearen Quantoren im Allgemeinen. Es stellte sich heraus, dass die Prädikatenlogik erster Stufe, erweitert durch Henkin-Quantoren, unvollständig ist. Das bedeutet, dass (wie in der Logik zweiter Ordnung) kein Axiom- und Regelsystem existiert in welchem alle wahren Sätze ableitbar sind. Dem vorliegenden Projekt gelang es Herleitungssysteme zu erstellen, die zumindest den Beweis der wichtigsten natürlichen Sätze mit nicht linearen Quantoren erlauben, sowie mit der beweistheoretischen Analyse dieser Herleitungssysteme. Für die Systeme sollen dabei insbesondere der Schnitteliminationssatz und Varianten des Satzes von Herbrand gezeigt werden. Die Möglichkeit Schnitte zu eliminieren ist wesentlich für die Analsyse von Beweisen erster Ordnung (Proof Mining).