Komplexitätstheorie in schwachen Arithmetiken

Dies ist ein Vorschlag zu einem Forschungsprojekt in Beweiskomplexität, ein Gebiet im Grenzbereich mathematischer Logik und der Theorie der Berechnungskomplexität. Allgemein gesprochen, geht es in der Beweiskomplexität darum, wie schwierig es ist, mathematische Theoreme zu beweisen. In der Aussagenlogik betrifft das hauptsächlich Abschätzungen der minimalen Länge von Beweisen gegebener Tautologien, in der Prädikatenlogik betrifft das die Charakterisierungen der deduktiven Stärke mathematischer Theorien. Für relativ starke aussagenlogische Kalküle, genannt Frege und Extended Frege, sind keine (nicht trivialen) untere Schranken an die Beweislänge bekannt. Ausserdem mangelt es an mathematischen Methoden, die Unabhängigkeit universeller Sätze von schwachen Arithmetiken zu zeigen. In beiden Fällen ist es sogar schwierig, auch nur vermutungsweise solche Tautologien beziehungsweise Sätze zu formulieren. Via einer Simulation von schwachen Arithmetiken in aussagenlogischen Kalkülen, sind beide Fragen eng miteinander verwandt. Beispielsweise simuliert Extended Frege eine schwache arithmetische Theorie, die das Argumentieren mit in Polynomialzeit berechenbaren Konzepten und Funktionen formalisiert. Diese Wissenslücken hängen damit zusammen, dass einige der grundlegenden Hypothesen der Komplexitätstheorie bislang unbewiesen sind. Eine prominente Vermutung besagt, dass solche Hypothesen selbst von schwachen Arithmetiken unabhängig sein könnten. Ein Beispiel ist die Hypothese, dass das berühmte NP-vollständigeErfüllbarkeitsproblemsuperpolynomielle Schaltkreiskomplexität hat. Unbeweisbarkeit dieser Hypothese in obiger Theorie würde bedeuten, dass ein Beweis der Hypothese zwangsweise Konzepte und Funktionen hoher Berechnungskomplxität verwenden muss. Auf der aussagenlogischen Seite sind die die Hypothese wiedergebenden Tautologien ein zentrales Beispiel solcher Tautologien, die durch sogenannte Beweiskomplexitätsgeneratoren gewonnen werden. In manchen Fällen lässt sich die Unabhängigkeit einer Aussage von einer schwachen Arithmetik dadurch zeigen,dass ihre Beweisbarkeit dieExistenzgewisser Skolemfunktionenmit niedriger Berechnungskomplexität implizieren würde, und dies wiederum mag anderen komplexitätstheoretischen Hypothesen widersprechen. Leider scheint dieser Ansatz nicht auf obiges Beispiel zur Schaltkreiskomplexität anwendbar zu sein. Eine Idee dieses Forschungsvorhabens besteht darin, dass man sich das Fehlschlagen dieses Ansatzes zunutze machen kann. Nämlich, wenn Skolemfunktionen existieren, dann kann man diese dazu verwenden wiederum neue, a priori noch schwierigere Tautologien zu produzieren, die dieselbe Hypothese formalisieren. Grob gesagt liegt das daran, dass bezeugende Funktionen erlauben, Quantoren zu eliminieren und so Formeln zu vereinfachen. Allgemein gesprochen ist das Ziel dieses Projekts, sowohl zum derzeitigen spärlichen Verständnis der angesprochenen Generatoren als auch zum Verständnis des Zusammenhangs von komplexitätstheoretischen Hypothesen einerseits und deren Beweisbarkeit in schwachen Arithmetiken andererseits beizutragen.

Die Grenzen effizienter Berechenbarkeit zu verstehen, ist eine der größten Herausforderungen in Wissenschaft und Gesellschaft. Die theoretische Komplexitätstheorie ist der Erforschung dieses generischen Ziels gewidmet, doch zentrale Fragen des Gebiets wie das berühmte P- versus-NP-Problem scheinen außer Reichweite zu sein. Das vorliegende Projekt betrachtete derartige Fragen aus der Perspektive der mathematischen Logik, genauer gesagt, aus der Perspektive der Theorie beschränkter Arithmetiken. Diese Theorien formalisieren verschiedene Grade algorithmisch behandelbaren logischen Schließens. Die Hauptergebnisse des Projekts umfassen 1. effizient konstruktive Beweise der Grenzen zentraler beschränkter Berechnungsmodelle, und 2. die Mitentwicklung eines neuen Ansatzes zum Verständnis starker uneingeschränkter Berechnungsmodelle und insbesondere ein Beitrag zu einem neuen Ansatz zur Lösung des P-versus-NP-Problems, der bisher bestehende Barrieren umgeht. Wir hoffen, dass dieser Beitrag zum theoretischen Verständnis effizienter Berechenbarkeit letztendlich dazu beitragen wird, effizientere Algorithmen für das alltägliche Leben zu entwickeln.