Abstrakte Maße schwacher Komplexität

Konkrete Komplexität beschreibt beispielsweise den Zeit- oder Speicherbedarf von Algorithmen mit Bezug auf den wirklichen Ablauf, wohingegen abstrakte Komplexität eine mathematische Begriffsbildung ist, die versucht, die ideellen Objekte zu charakterisieren, die der konkreten Komplexität innewohnen. Das Leitmotiv für abstrakte Komplexitätsmaße ist die beweistheoretische Ordinalzahl epsilon_0, die schon in der berühmten Arbeit von Gerhard Gentzen (1936) zur Rettung von Hilberts gescheitertem Programm vorkommt. Beweistheoretische Ordinalzahlen stellen mathematische Beschreibungen der Beweis- und Berechnungskraft von mathematischen Theorien und Klassen subrekursiver Funktionen dar, und bilden damit ein Paradigma abstrakter Komplexität im obigen Sinne. Das Konzept der beweistheoretischen Ordinalzahl wird im Rahmen schwacher Berechnungsklassen durch dynamische Ordinalzahlen adäquat adaptiert; dynamische Ordinalzahlen reflektieren die Beweiskraft von schwachen Teiltheorien der Peano Arithmetik ("Bounded Arithmetic"), indem sie diese eng mit aussagenlogischen Beweissystemen verknüpfen. Im Rahmen des Projektes ist beabsichtigt, die dynamischen Ordinalzahlen zu abstrakten Maßen schwacher Komplexität im obigen Sinne zu verallgemeinern. Insbesondere sollen so die definierbaren Funktionen in Theorien der Bounded Arithmetic intrinsisch durch abstrakte Maße beschrieben werden. Zu diesem Zweck werden die tiefliegenden Zusammenhänge zu starken unteren Schranken aussagenlogischer Beweissysteme genutzt, insbesondere soll die aussagenlogische Beweiskomplexität der Ramsey-Eigenschaft bestimmt und benutzt werden. Als Hauptergebnis soll und wird das vorliegende Projekt zu einem besseren Verständnis der inhärenten Komplexität von schwachen Komplexitätsklassen und damit zusammenhängenden logischen Beschreibungen führen. Anwendungsgebiete sind alle Bereiche, die mit schwachen Komplexitätsklassen verbunden sind, zum Beispiel die Untersuchung Deskriptiver Komplexitätsklassen oder auch das Automatische Beweisen, dessen Hauptformalismus (der Resolutionskalkül) auf einem spezifischen aussagenlogischen Beweissystem basiert.