Logische Komplexität und Termstruktur

In der Mathematik sind wir es gewohnt, über eine Vielzahl verschiedener, oft hoch abstrakter, Objekte zu sprechen und zu schreiben, wie z.B. über unendliche Menge, reelle Zahlen, reellwertige Funktionen, Operatoren die solche Funktionen transformieren, usw. Allerdings tun wir das auf eine inhärent endliche Art und Weise: jede Definition, jeder Beweis, jeder mathematische Text ist eine endliche Folge von Zeichen aus einem endlichen Alphabet. Diese einfache aber bedeutende Einsicht liegt an der Wurzel der Entwicklung der mathematischen Logik am Beginn des 20. Jahrhunderts, die unser Verständnis der Grundlagen der Mathematik revolutioniert hat. Dieses Projekt setzt diese Tradition fort indem es mathematische Methoden zur Analyse der Sprache der Mathematik einsetzt. Es hat zum Ziel diese Methodologie zu erweitern indem die für solche Analysen zur Verfügung stehenden mathematischen Techniken erweitert werden. Diese neu zu entwickelten Techniken werden eingesetzt werden um neue Einsichten in die Grundlagen der Mathematik und in der Philosophie der Praxis der Mathematik zu gewinnen. Das konkrete Thema dieses Projekts ist die Analyse der Struktur formaler Beweise und, genauer, der Rolle der Struktur von Termen in prädikatenlogischen Beweisen und deren Interaktion mit der logischen Komplexität von Formeln. Die neuen Techniken die dieses Projekt in der Beweistheorie und in den Grundlagen der Mathematik entwickeln wird kommen aus der Automatentheorie und der Beschreibungskomplexität. Indem wir ein Strukturtheorem beweisen, werden wir zeigen wie einem formalen Beweis eine formale Baumgrammatik zugeordnet werden kann, die die Struktur des Beweises auf konzise und logikfreie Weise darstellt. Die Bedeutung eines solchen Resultats liegt darin, dass wir dadurch nicht nur einen neue Repräsentation von Herbrand-Expansionen erhalten, sondern eine die konzeptuell einfach ist aber gleichzeitig in Größe und Struktur dem ursprünglichen komplexen Beweis eng verbunden ist. Dadurch bietet sie eine ideale Abstraktion für Analyse der Termschicht eines Beweises. Das erlaubt sowohl die Entwicklung neuer theoretischer Resultate als auch von Algorithmen die direkt auf dieser neuartigen Repräsentation arbeiten. Die vollständige Entwicklung dieser innovativen Techniken ist der Schlüssel um tiefgründige Fragen über die Grundlagen der Mathematik und in der Philosophie der Praxis der Mathematik anzugehen, wie zum Beispiel: Was ist das Verhältnis zwischen abstrakten Beweisen und konkreten Rechnungen? Welche Rolle spielt implizite Information in Definitionen? Wieso bevorzugen wir funktionale Notation über Alternativen? Gibt es komplexitätstheoretische Gründe für die Verwendung von Konzepten in Beweisen?