Beweistheorie mittels beschränkter Sequenzialkalküle

Die mathematische Formalisierung eines Argumentationssystems wird als Logik bezeichnet. Logik spielt in zahlreichen Bereichen der Informatik, der mathematischen Logik, der Linguistik, der Philosophie und darüber hinaus eine herausragende Rolle. Neben der Vielfalt dieser Bereiche sind auch die Argumentationstypen, welche in den jeweiligen Szenarien zum Tragen kommen, unterschiedlich. Es gibt daher keine einheitliche Logik die in allen Szenarien anwendbar ist. Bei der Untersuchung einer Logik stellen sich mehrere wichtige Fragen. Zum Beispiel: Können wir auf effiziente Art und Weise feststellen, ob eine bestimmte Aussage (Argumentation) eine Konsequenz der Logik ist? Was ist die Komplexität eines solchen Algorithmus? Wie verhält sich die Logik zu anderen Logiken in ihrem Umfeld? Zur Beantwortung solcher Fragen haben sich Beweissysteme als nützlich erwiesen. Es handelt sich hierbei um mathematische Formalismen, die (in einem abstrakten Sinn) die Beweise genau jener Aussagen erzeugen können, welche Konsequenzen der Logik sind. Gerhard Gentzen entwarf im Jahr 1935 für mehrere bedeutende Logiken ein elegantes Beweissystem namens "Sequenzenkalkül", welches sich durch die Eigenschaft der "Analytizität" auszeichnet. Vereinfacht gesagt bedeutet Analytizität, dass sich der Beweis einer komplexen Aussage stets aus den Beweisen einfacherer Aussagen zusammenfügen lässt. Auf diese Weise wird die Komplexität einer Aussage mit der Struktur ihres Beweises in Bezug gesetzt. Leider ist es für die meisten interessanten Logiken schwierig oder sogar unmöglich, einen Sequenzenkalkül mit der Analytizitätseigenschaft zu konstruieren. Aus diesem Grund hat man sich in letzter Zeit zumeist auf die Entwicklung komplizierter neuer Beweissysteme konzentriert, die den Sequenzenkalkül ersetzen. Dies hat allerdings seinen Preis: Ungeachtet der Analytizitätseigenschaft dieser Beweissysteme eignen sie sich aufgrund ihrer Komplexität nur bedingt zur Untersuchung logischer Fragen. Im vorliegenden Projekt soll untersucht werden, wie man komplizierte Beweissysteme mit der Analytizitätseigenschaft auf Sequenzenkalküle zurückführen kann. Die so erhaltenen Sequenzenkalküle werden verschiedene Eigenschaften haben, die zwar schwächer als Analytizität, aber dennoch nützlich sind. Solche Beweissysteme werden "beschränkte Sequenzenkalküle" genannt. Das Projekt wird den Grundstein für die Erforschung beschränkter Sequenzenkalküle legen und sie zum Studium logischer Fragen verwenden. Schlussendlich werden wir untersuchen, inwiefern beschränkte Sequenzenkalküle als einheitlicher mathematischer Formalismus für die Konstruktion von Beweissystemen und die Untersuchung von Logiken dienen können.