Ordinalanalyse

Die Ordinalanalyse misst die Stärke einer formalen Theorie durch die kleinste Ordinalzahl, von der die Theorie nicht beweisen kann, dass sie wohlgeordnet ist, und weist jeder Theorie eine präzise beweistheoretische Ordinalzahl zu.

Definition

Die beweistheoretische Ordinalzahl einer Theorie ist das Supremum der Ordnungstypen der rekursiven Wohlordnungen, deren Wohlfundiertheit die Theorie beweisen kann; Ordinalanalyse ist das Programm zur Berechnung dieser Invarianten und deren Verwendung zum Vergleich und zur Kalibrierung von Theorien.

Scope

Dieses Thema behandelt Genzens Konsistenzbeweis für die Arithmetik unter Verwendung transfinitter Induktion bis zur Ordinalzahl Epsilon-Null, Systeme der Ordinalzahlnotation, die beweistheoretische Ordinalzahl als Invariante einer Theorie, die Methoden der Schnittelimination für infinitäre Ableitungen und die Analyse von Teilsystemen der Arithmetik und prädikativen Theorien.

Core questions

• Wie misst eine Ordinalzahl die Stärke einer arithmetischen Theorie?
• Warum beweist die transfinite Induktion bis Epsilon-Null die Konsistenz der Arithmetik?
• Wie werden Ordinalzahlnotationen definiert, sodass sie endlich begründet werden können?
• Welche Ordinalzahlen entsprechen den Standard-Subsystemen der Arithmetik zweiter Ordnung?

Key theories

Gentzen-Konsistenzbeweis

Gentzen bewies die Konsistenz der Arithmetik erster Ordnung, indem er Beweisen Ordinalzahlen unterhalb von Epsilon-Null zuwies und zeigte, dass die Schnittreduktion diese verringert, sodass die transfinite Induktion bis Epsilon-Null die Konsistenz bescheinigt.

Beweistheoretische Ordinalzahl

Jede hinreichend starke Theorie hat eine charakteristische Ordinalzahl, die die transfinite Induktion erfasst, die sie rechtfertigen kann, und bietet eine feinkörnige und weitgehend lineare Skala der logischen Stärke.

Ordinalzahl-Notationssysteme

Große Ordinalzahlen werden durch endliche syntaktische Notationen, wie die Veblen-Funktionen und Kollapsfunktionen, dargestellt, was die Manipulation unendlicher Ordinalzahlen innerhalb finiter oder arithmetischer Theorien ermöglicht.

Clinical relevance

Die Ordinalanalyse liefert das raffinierteste verfügbare Maß für die Stärke mathematischer Theorien: Sie legt genau fest, welche transfiniten Induktionen eine Theorie benötigt, klassifiziert die beweisbar rekursiven Funktionen einer Theorie und liefert relative Konsistenzinformationen, die jene ergänzen, die aus großen Kardinalzahlen gewonnen werden.

History

Genzens Konsistenzbeweise für die Arithmetik von 1936 und 1938 führten die Ordinalanalyse durch transfinite Induktion bis Epsilon-Null ein. Schuette, Feferman und andere erweiterten die Methode auf prädikative Theorien und verzweigte Analysen, und die Entwicklung von Kollapsfunktionen drängte die Ordinalanalyse später in starke imprädikative Systeme vor.

Key figures

• Gerhard Gentzen
• Kurt Schuette
• Solomon Feferman
• Wolfram Pohlers

Seminal works

• pohlers2009
• takeuti1987
• schutte1977

Frequently asked questions

Was ist die beweistheoretische Ordinalzahl der Arithmetik erster Ordnung?

Es ist Epsilon-Null, die Grenze des Turms von Omega-Exponentialfunktionen. Die Arithmetik erster Ordnung beweist transfinite Induktion bis zu jeder Ordinalzahl unterhalb von Epsilon-Null, aber nicht bis Epsilon-Null selbst, was genau das Prinzip ist, das Gentzen verwendete, um ihre Konsistenz zu beweisen.

Wie hängt die Ordinalanalyse mit der Unvollständigkeit zusammen?

Gödels zweiter Satz besagt, dass die Arithmetik ihre eigene Konsistenz nicht beweisen kann. Die Ordinalanalyse identifiziert das zusätzliche Prinzip, die transfinite Induktion bis Epsilon-Null, das sie beweist, und misst dadurch präzise, wie weit über die Theorie hinaus man gehen muss, um ihre Konsistenz festzustellen.