Semantische Charakterisierung der Schnittelimination

Schnittelimination ist eine der wichtigsten Techniken der Beweistheorie. Grob gesprochen erzeugt die Schnittelimination aus einem Beweis einen Beweis ohne Lemmata, der im wesentlichen aus den syntaktischen Bestandteilen des bewiesenen Satzes aufgebaut ist. Seit ihrer Einführung im Jahr 1934 sind Sequenzenkalküle eine der bevorzugten Instrumente der Formalisierung des Schließens in Logiken. Dieses Instrument ist jedoch nicht geeignet alle nützlichen und interessanten Logiken zu untersuchen. Aus diesem Grund wurde in den letzten Dekaden eine große Anzahl von Varianten und Erweiterungen des Gentzenschen Sequenzenkalküls eingeführt. Unter diesen gelten Hypersequenzenkalküle als besonders elegante und einfache Grundlage für "logical engineering" mit Anwendung auf zahlreiche nichtklassische Logiken. Ziel des vorliegenden Projektes ist eine semantische Charakterisierung der Schnittelimination in Sequenzen- und Hypersequenzenkalkülen. Damit ist die Formulierung von syntaktischen und semantischen Kriterien gemeint, die -- falls erfüllt -- eine bevorzugte Variante der Schnittelimination für den gegebenen Kalkül garantieren, andernfalls die Konstruktion eines Gegenbeispiels zu dieser bevorzugten Schnittelimination erlauben. Dabei stehen folgende Fragen im Mittelpunkt: Was sind natürliche Eigenschaften für Regeln, die Schnittelimination erhalten? Gibt es eine uniforme Methode um für eine große Klasse von Sequenten- und Hypersequenkalkülen die Eliminierbarkeit der Schnitte zu beweisen oder zu widerlegen? Die entscheidenden Vorteile einer solchen Methode wären: 1. Erleichterung des Nachweises der Schnittelimination für neue Kalküle und der Erstellung von analytischen Kalkülen für neue Logiken. 2. Möglichkeit der automatischen Erzeugung von Schnitteliminationsmethoden und der automatischen Überprüfung der zugehörigen formalen Kriterien.

Schnittelimination ist eine der wichtigsten Techniken der Beweistheorie. Grob gesprochen erzeugt die Schnittelimination aus einem Beweis einen Beweis ohne Lemmata, der im wesentlichen aus den syntaktischen Bestandteilen des bewiesenen Satzes aufgebaut ist. Seit ihrer Einführung im Jahr 1934 sind Sequenzenkalküle eine der bevorzugten Instrumente der Formalisierung des Schließens in Logiken. Dieses Instrument ist jedoch nicht geeignet alle nützlichen und interessanten Logiken zu untersuchen. Aus diesem Grund wurde in den letzten Dekaden eine große Anzahl von Varianten und Erweiterungen des Gentzenschen Sequenzenkalküls eingeführt. Unter diesen gelten Hypersequenzenkalküle als besonders elegante und einfache Grundlage für "logical engineering" mit Anwendung auf zahlreiche nichtklassische Logiken. Ziel des vorliegenden Projektes ist eine semantische Charakterisierung der Schnittelimination in Sequenzen- und Hypersequenzenkalkülen. Damit ist die Formulierung von syntaktischen und semantischen Kriterien gemeint, die - falls erfüllt - eine bevorzugte Variante der Schnittelimination für den gegebenen Kalkül garantieren, andernfalls die Konstruktion eines Gegenbeispiels zu dieser bevorzugten Schnittelimination erlauben. Dabei stehen folgende Fragen im Mittelpunkt: Was sind natürliche Eigenschaften für Regeln, die Schnittelimination erhalten? Gibt es eine uniforme Methode um für eine große Klasse von Sequenten- und Hypersequenkalkülen die Eliminierbarkeit der Schnitte zu beweisen oder zu widerlegen? Die entscheidenden Vorteile einer solchen Methode wären: 1. Erleichterung des Nachweises der Schnittelimination für neue Kalküle und der Erstellung von analytischen Kalkülen für neue Logiken. 2. Möglichkeit der automatischen Erzeugung von Schnitteliminationsmethoden und der automatischen Überprüfung der zugehörigen formalen Kriterien.