Rückmathematik ist ein Programm in der mathematischen Logik, die sich bemüht zu bestimmen, welche Axiome erforderlich sind, Lehrsätze der Mathematik zu beweisen. Seine Definieren-Methode kann als das "Gehen umgekehrt von den Lehrsätzen bis die Axiome", im Gegensatz zur gewöhnlichen mathematischen Praxis von abstammenden Lehrsätzen von Axiomen kurz beschrieben werden. Das Rückmathematik-Programm wurde dadurch ahnen lassen läuft auf Mengenlehre wie der klassische Lehrsatz hinaus, dass das Axiom der Wahl und des Lemmas von Zorn über die ZF Mengenlehre gleichwertig ist. Die Absicht der Rückmathematik ist jedoch, mögliche Axiome von gewöhnlichen Lehrsätzen der Mathematik aber nicht mögliche Axiome für die Mengenlehre zu studieren.

Rückmathematik wird gewöhnlich mit Subsystemen der Arithmetik der zweiten Ordnung ausgeführt, wo viele seiner Definitionen und Methoden durch die vorherige Arbeit in der konstruktiven Analyse und Probetheorie begeistert werden. Der Gebrauch der Arithmetik der zweiten Ordnung erlaubt auch vielen Techniken aus der recursion Theorie, verwendet zu werden; viele laufen auf Rückmathematik hinaus haben entsprechende Ergebnisse in der berechenbaren Analyse.

Das Programm wurde dadurch gegründet. Ein normativer Verweis für das Thema ist.

Allgemeine Grundsätze

In der Rückmathematik fängt man mit einer Fachwerk-Sprache und einer Grundtheorie — einem Kernaxiom-System an — der zu schwach ist, um die meisten Lehrsätze zu beweisen, könnte man sich für, aber noch stark genug interessieren, um die Definitionen zu entwickeln, die notwendig sind, um diese Lehrsätze festzusetzen. Zum Beispiel, um den Lehrsatz zu studieren, "Hat jede begrenzte Folge von reellen Zahlen ein Supremum" es ist notwendig, ein Grundsystem zu verwenden, das von reellen Zahlen und Folgen von reellen Zahlen sprechen kann.

Für jeden Lehrsatz, der im Grundsystem festgesetzt werden kann, aber im Grundsystem nicht nachweisbar ist, ist die Absicht, das besondere Axiom-System zu bestimmen (stärker als das Grundsystem), der notwendig ist, um diesen Lehrsatz zu beweisen. Um zu zeigen, dass ein System S erforderlich ist, einen Lehrsatz T zu beweisen, sind zwei Beweise erforderlich. Der erste Beweis zeigt, dass T von S nachweisbar ist; das ist ein gewöhnlicher mathematischer Beweis zusammen mit einer Rechtfertigung, dass sie im System S ausgeführt werden kann. Der zweite Beweis, der als eine Umkehrung bekannt ist, zeigt, dass T selbst S einbezieht; dieser Beweis wird im Grundsystem ausgeführt. Die Umkehrung stellt dass kein Axiom-System S&prime fest; das streckt sich aus das Grundsystem kann schwächer sein als S, während es sich noch T erweist.

Gebrauch der Arithmetik der zweiten Ordnung

Der grösste Teil der Rückmathematik-Forschung konzentriert sich auf Subsysteme der Arithmetik der zweiten Ordnung. Der Körper der Forschung in der Rückmathematik hat festgestellt, dass schwache Subsysteme der Arithmetik der zweiten Ordnung genügen, um fast die ganze Studentenniveau-Mathematik zu formalisieren. In der Arithmetik der zweiten Ordnung müssen alle Gegenstände entweder als natürliche Zahlen oder als Sätze von natürlichen Zahlen vertreten werden. Zum Beispiel, um Lehrsätze über reelle Zahlen zu beweisen, müssen die reellen Zahlen als Cauchyfolgen von rationalen Zahlen vertreten werden, von denen jede als eine Reihe von natürlichen Zahlen vertreten werden kann.

Die in der Rückmathematik meistenteils betrachteten Axiom-Systeme werden mit Axiom-Schemas genannt Verständnis-Schemas definiert. Solch ein Schema stellt fest, dass jeder Satz von durch eine Formel einer gegebenen Kompliziertheit definierbaren natürlichen Zahlen besteht. In diesem Zusammenhang wird die Kompliziertheit von Formeln mit der arithmetischen Hierarchie und analytischen Hierarchie gemessen.

Der Grund, dass Rückmathematik mit der Mengenlehre als ein Grundsystem nicht ausgeführt wird, besteht darin, dass die Sprache der Mengenlehre zu ausdrucksvoll ist. Äußerst komplizierte Sätze von natürlichen Zahlen können durch einfache Formeln auf der Sprache der Mengenlehre definiert werden (der über willkürliche Sätze messen kann). Im Zusammenhang der Arithmetik der zweiten Ordnung gründen Ergebnisse wie der Lehrsatz des Postens eine nahe Verbindung zwischen der Kompliziertheit einer Formel und der (nicht) Berechenbarkeit des Satzes, den es definiert.

Eine andere Wirkung, Arithmetik der zweiten Ordnung zu verwenden, ist das Bedürfnis, allgemeine mathematische Lehrsätze auf Formen einzuschränken, die innerhalb der Arithmetik ausgedrückt werden können. Zum Beispiel kann Arithmetik der zweiten Ordnung den Grundsatz "Jeder zählbare Vektorraum ausdrücken hat eine Basis", aber es kann den Grundsatz "Jeder Vektorraum nicht ausdrücken hat eine Basis". In praktischen Begriffen bedeutet das, dass Lehrsätze der Algebra und combinatorics auf zählbare Strukturen eingeschränkt werden, während Lehrsätze der Analyse und Topologie auf trennbare Räume eingeschränkt werden. Viele Grundsätze, die das Axiom der Wahl in ihrer allgemeinen Form einbeziehen (wie "Jeder Vektorraum hat eine Basis"), werden nachweisbar in schwachen Subsystemen der Arithmetik der zweiten Ordnung, wenn sie eingeschränkt werden. Zum Beispiel "hat jedes Feld einen algebraischen Verschluss", ist in der ZF Mengenlehre nicht nachweisbar, aber die eingeschränkte Form "jedes zählbare Feld hat einen algebraischen Verschluss" ist in RCA, das schwächste in der Rückmathematik normalerweise verwendete System nachweisbar.

Die großen fünf Subsysteme der zweiten Ordnungsarithmetik

Die zweite Ordnungsarithmetik ist eine formelle Theorie der natürlichen Zahlen und Sätze von natürlichen Zahlen. Viele mathematische Gegenstände, wie zählbare Ringe, Gruppen, und Felder, sowie Punkte in wirksamen polnischen Räumen, können als Sätze von natürlichen Zahlen und modulo vertreten werden diese Darstellung kann in der zweiten Ordnungsarithmetik studiert werden.

Rückmathematik macht von mehreren Subsystemen der zweiten Ordnungsarithmetik Gebrauch. Ein typischer Rückmathematik-Lehrsatz zeigt, dass ein besonderer mathematischer Lehrsatz T zu einem besonderen Subsystem S der zweiten Ordnungsarithmetik über ein schwächeres Subsystem B gleichwertig ist. Dieses schwächere System B ist als das Grundsystem für das Ergebnis bekannt; in der Größenordnung von der Rückmathematik resultieren, um zu haben

wenn es

bedeutet, muss dieses System nicht selbst im Stande sein, den mathematischen Lehrsatz T zu beweisen.

beschreibt fünf besondere Subsysteme der zweiten Ordnungsarithmetik, die er die Großen Fünf nennt, die oft in der Rückmathematik vorkommen. In der Größenordnung von der zunehmenden Kraft werden diese Systeme durch den initialisms RCA, WKL, ACA, ATR und genannt

Π-CA.

Der folgende Tisch fasst die "großen fünf" Systeme zusammen

Die Subschrift in diesen Namen bedeutet, dass das Induktionsschema aus dem vollen Induktionsschema der zweiten Ordnung eingeschränkt worden ist. Zum Beispiel schließt ACA das Induktionsaxiom (0X  n (nX  n+1X))  n nX ein. Das zusammen mit dem vollen Verständnis-Axiom der zweiten Ordnungsarithmetik bezieht das volle Induktionsschema der zweiten Ordnung ein, das durch den universalen Verschluss (φ (0)  n (φ (n)  φ (n+1)))  n φ (n) für jede zweite Ordnungsformel φ gegeben ist. Jedoch hat ACA das volle Verständnis-Axiom nicht, und die Subschrift ist eine Gedächtnishilfe, dass es das volle Induktionsschema der zweiten Ordnung auch nicht hat. Diese Beschränkung ist wichtig: Systeme mit der eingeschränkten Induktion haben bedeutsam niedrigere probetheoretische Ordnungszahlen als Systeme mit dem vollen Induktionsschema der zweiten Ordnung.

Das Grundsystem RCA

RCA ist das Bruchstück der Arithmetik der zweiten Ordnung, deren Axiome die Axiome der Arithmetik von Robinson, Induktion für &Sigma sind; Formeln und Verständnis für Δ Formeln.

Das Subsystem RCA ist dasjenige, das meistens als ein Grundsystem für die Rückmathematik verwendet ist. Die Initialen "RCA" treten "für rekursives Verständnis-Axiom", wo "rekursiv", Mittel "berechenbar", als in der rekursiven Funktion ein. Dieser Name wird verwendet, weil RCA informell zur "berechenbaren Mathematik" entspricht. Insbesondere jeder Satz von natürlichen Zahlen, die, wie man beweisen kann, in RCA bestehen, ist berechenbar, und so ist jeder Lehrsatz, der andeutet, dass nichtberechenbare Sätze bestehen, in RCA nicht nachweisbar. In diesem Ausmaß ist RCA ein konstruktives System, obwohl es den Anforderungen des Programms von constructivism nicht entspricht, weil es eine Theorie in der klassischen Logik einschließlich der ausgeschlossenen Mitte ist.

Trotz seiner scheinbaren Schwäche (irgendwelche nichtberechenbaren Sätze nicht zu beweisen, bestehen), ist RCA genügend, um mehrere klassische Lehrsätze zu beweisen, die deshalb nur minimale logische Kraft verlangen. Diese Lehrsätze sind gewissermaßen unter der Reichweite des Rückmathematik-Unternehmens, weil sie bereits im Grundsystem nachweisbar sind. Die klassischen in RCA nachweisbaren Lehrsätze schließen ein:

• Grundlegende Eigenschaften der natürlichen Zahlen, ganzen Zahlen und rationalen Zahlen (zum Beispiel, dass die letzte Form ein bestelltes Feld).
• Grundlegende Eigenschaften der reellen Zahlen (sind die reellen Zahlen Archimedean bestelltes Feld; jede verschachtelte Folge von geschlossenen Zwischenräumen, deren Längen zur Null neigen, hat einen einzelnen Punkt in seiner Kreuzung; die reellen Zahlen sind nicht zählbar).
• Der Baire Kategorie-Lehrsatz für einen ganzen trennbaren metrischen Raum (ist die Trennbarkeitsbedingung notwendig, um sogar den Lehrsatz auf der Sprache der Arithmetik der zweiten Ordnung festzusetzen).
• Der Zwischenwertlehrsatz auf dauernden echten Funktionen.
• Der Banach-Steinhaus Lehrsatz für eine Folge von dauernden geradlinigen Maschinenbedienern auf trennbaren Banachräumen.
• Eine schwache Version des Vollständigkeitslehrsatzes von Gödel (für eine Reihe von Sätzen, auf einer zählbaren Sprache, die bereits unter der Folge geschlossen wird).
• Die Existenz eines algebraischen Verschlusses für ein zählbares Feld (aber nicht seine Einzigartigkeit).
• Die Existenz und Einzigartigkeit des echten Verschlusses eines zählbaren bestellten Feldes.

Der Teil der ersten Ordnung von RCA (die Lehrsätze des Systems, die keine Satz-Variablen einschließen) ist der Satz von Lehrsätzen der ersten Ordnung Arithmetik von Peano mit der auf Σ Formeln beschränkten Induktion. Es entspricht nachweisbar, wie RCA, in der vollen ersten Ordnung Arithmetik von Peano ist.

Das Lemma des schwachen Königs WKL

Der Subsystem-WKL besteht aus RCA plus eine schwache Form des Lemmas von König, nämlich die Behauptung, dass jeder unendliche Subbaum des vollen binären Baums (der Baum aller begrenzten Folgen von 0's und 1's) einen unendlichen Pfad hat. Dieser Vorschlag, der als das Lemma des schwachen Königs bekannt ist, ist leicht, auf der Sprache der Arithmetik der zweiten Ordnung festzusetzen. WKL kann auch als der Grundsatz der Σ Trennung definiert werden (gegeben zwei Σ Formeln einer freien Variable n, die exklusiv sind, gibt es eine Klasse, die den ganzen n Zufriedenheit von derjenigen und keinem n Zufriedenheit vom anderen enthält).

Die folgende Bemerkung auf der Fachsprache ist in der Ordnung. Der Begriff "das Lemma des schwachen Königs" bezieht sich auf den Satz, der sagt, dass jeder unendliche Subbaum des binären Baums einen unendlichen Pfad hat. Wenn dieses Axiom zu RCA hinzugefügt wird, wird das resultierende Subsystem WKL genannt. Eine ähnliche Unterscheidung zwischen besonderen Axiomen, einerseits, und Subsysteme einschließlich der grundlegenden Axiome und Induktion wird andererseits für die stärkeren Subsysteme gemacht, die unten beschrieben sind.

Gewissermaßen ist das Lemma des schwachen Königs eine Form des Axioms der Wahl (obwohl, wie festgesetzt, es in der klassischen Zermelo-Fraenkel Mengenlehre ohne das Axiom der Wahl bewiesen werden kann). Es ist in einigen konstruktiven Bedeutungen des Wortes nicht konstruktiv gültig.

Um zu zeigen, dass WKL wirklich stärker ist als (nicht nachweisbar in) RCA, ist es genügend, einen Lehrsatz von WKL auszustellen, der andeutet, dass nichtberechenbare Sätze bestehen. Das ist nicht schwierig; WKL bezieht die Existenz ein, Sätze für effektiv untrennbaren rekursiv enumerable Sätze zu trennen.

Es stellt sich heraus, dass RCA und WKL denselben Teil der ersten Ordnung haben, bedeutend, dass sie dieselben Sätze der ersten Ordnung beweisen. WKL kann eine große Anzahl von klassischen mathematischen Ergebnissen beweisen, die aus RCA jedoch nicht folgen. Diese Ergebnisse sind nicht expressible die so ersten Ordnungsbehauptungen, aber können ausgedrückt werden wie Behauptungen der zweiten Ordnung.

Die folgenden Ergebnisse sind zum Lemma des schwachen Königs und so zu WKL über RCA gleichwertig:

• Der Lehrsatz von Heine-Borel für die geschlossene Einheit echter Zwischenraum, im folgenden Sinn: Jede Bedeckung durch eine Folge von offenen Zwischenräumen hat eine begrenzte Subbedeckung.
• Der Lehrsatz von Heine-Borel für ganze völlig begrenzte trennbare metrische Räume (wo Bedeckung durch eine Folge von offenen Bällen ist).
• Eine dauernde echte Funktion auf dem geschlossenen Einheitszwischenraum (oder auf jedem metrischen trennbaren Kompaktraum, als oben) wird begrenzt (oder: Begrenzt und erreicht seine Grenzen).
• Einer dauernden echten Funktion auf dem geschlossenen Einheitszwischenraum kann durch Polynome (mit vernünftigen Koeffizienten) gleichförmig näher gekommen werden.
• Eine dauernde echte Funktion auf dem geschlossenen Einheitszwischenraum ist gleichförmig dauernd.
• Eine dauernde echte Funktion auf dem geschlossenen Einheitszwischenraum ist Riemann integrable.
• Der Brouwer hat Punkt-Lehrsatz (für dauernde Funktionen auf einem begrenzten Produkt von Kopien des geschlossenen Einheitszwischenraums) befestigt.
• Der trennbare Hahn-Banach Lehrsatz in der Form: Eine begrenzte geradlinige Form auf einem Subraum eines trennbaren Banachraums streckt sich bis zu eine begrenzte geradlinige Form auf dem ganzen Raum aus.
• Der Kurve-Lehrsatz von Jordan
• Der Vollständigkeitslehrsatz von Gödel (für eine zählbare Sprache).
• Determinacy für den offenen (oder sogar clopen) Spiele auf {0,1} der Länge ω.
• Jeder zählbare Ersatzring hat ein Hauptideal.
• Jedes zählbare formell echte Feld ist orderable.
• Einzigartigkeit des algebraischen Verschlusses (für ein zählbares Feld).

Arithmetisches Verständnis ACA

ACA ist RCA plus das Verständnis-Schema für arithmetische Formeln (der manchmal das "arithmetische Verständnis-Axiom" genannt wird). D. h. ACA erlaubt uns, den Satz von natürlichen Zahlen zu bilden, die eine willkürliche arithmetische Formel befriedigen (ein ohne bestimmte Satz-Variablen, obwohl vielleicht enthaltend Parameter aufgestellt hat). Wirklich genügt es, um zu RCA das Verständnis-Schema für Σ Formeln hinzuzufügen, um volles arithmetisches Verständnis zu erhalten.

Der Teil der ersten Ordnung von ACA ist genau erste Ordnung Arithmetik von Peano; ACA ist eine konservative Erweiterung der ersten Ordnung Arithmetik von Peano. Die zwei Systeme sind nachweisbar (in einem schwachen System) equiconsistent. Von ACA kann als ein Fachwerk der aussagenden Mathematik gedacht werden, obwohl es aussagend nachweisbare Lehrsätze gibt, die in ACA nicht nachweisbar sind. Die meisten grundsätzlichen Ergebnisse über die natürlichen Zahlen und viele andere mathematische Lehrsätze, können in diesem System bewiesen werden.

Eine Weise zu sehen, dass ACA stärker ist als WKL, soll ein Modell von WKL ausstellen, der alle arithmetischen Sätze nicht enthält. Tatsächlich ist es möglich, ein Modell von WKL zu bauen, der völlig aus niedrigen Sätzen mit dem niedrigen Basislehrsatz besteht, da niedrige Sätze hinsichtlich niedriger Sätze niedrig sind.

Die folgenden Behauptungen sind zu ACA gleichwertig

über RCA:

• Die folgende Vollständigkeit der reellen Zahlen (hat jede begrenzte zunehmende Folge von reellen Zahlen eine Grenze).
• Der Bolzano-Weierstrass Lehrsatz.
• Der Lehrsatz von Ascoli: Jede begrenzte equicontinuous Folge von echten Funktionen auf dem Einheitszwischenraum hat eine gleichförmig konvergente Subfolge.
• Jeder zählbare Ersatzring hat ein maximales Ideal.
• Jeder zählbare Vektorraum über den rationals (oder über jedes zählbare Feld) hat eine Basis.
• Jedes zählbare Feld hat eine Überlegenheitsbasis.
• Das Lemma von König (für willkürliche sich begrenzt verzweigende Bäume, im Vergleich mit der schwachen Version, die oben beschrieben ist).
• Verschiedene Lehrsätze in combinatorics, wie bestimmte Formen des Lehrsatzes von Ramsey.

Arithmetischer transfiniter Recursion ATR

Der System-ATR fügt zu ACA ein Axiom hinzu, das informell feststellt, dass irgendwelcher arithmetisch funktionell (Bedeutung jeder arithmetischen Formel mit einer freien Zahl-Variable n und einer freien Klassenvariable X, gesehen als der Maschinenbediener, der X zum Satz von n Zufriedenheit der Formel bringt), transfinit entlang jedem zählbaren gut Einrichtung wiederholt werden kann, die mit jedem Satz anfängt. ATR ist über ACA zum Grundsatz der Σ Trennung gleichwertig. ATR ist impredicative, und hat die probetheoretische Ordnungszahl, das Supremum von diesem von aussagenden Systemen.

ATR beweist die Konsistenz von ACA, und so durch den Lehrsatz von Gödel ist es ausschließlich stärker.

Die folgenden Behauptungen sind zu gleichwertig

ATR über RCA:

• Irgendwelche zwei zählbar gut Einrichtung sind vergleichbar. D. h. sie sind isomorph, oder man ist zu einem richtigen anfänglichen Segment vom anderen isomorph.
• Der Lehrsatz von Ulm für zählbare reduzierte Gruppen von Abelian.
• Der vollkommene Satz-Lehrsatz, der feststellt, dass jede unzählbare geschlossene Teilmenge eines ganzen trennbaren metrischen Raums einen vollkommenen geschlossenen Satz enthält.
• Der Trennungslehrsatz von Lusin (im Wesentlichen Σ Trennung).
• Determinacy für offene Sätze im Raum von Baire.

Π-Verständnis Π-CA

Π-CA ist stärker als arithmetischer transfiniter recursion und ist völlig impredicative. Es besteht aus RCA plus das Verständnis-Schema für Π Formeln.

Gewissermaßen, Π-CA Verständnis ist zu arithmetischem transfinitem recursion (Σ Trennung), wie ACA zum Lemma des schwachen Königs (Σ Trennung) ist. Es ist zu mehreren Behauptungen der beschreibenden Mengenlehre gleichwertig, deren Beweise von stark impredicative Argumente Gebrauch machen; diese Gleichwertigkeit zeigt, dass diese impredicative Argumente nicht entfernt werden können.

Die folgenden Lehrsätze sind zu Π-CA über RCA gleichwertig:

• Der Lehrsatz des Kantoren-Bendixson (ist jeder geschlossene Satz von reals die Vereinigung eines vollkommenen Satzes und eines zählbaren Satzes).
• Jede zählbare abelian Gruppe ist die direkte Summe einer teilbaren Gruppe und einer reduzierten Gruppe.

Zusätzliche Systeme

• Schwächere Systeme als rekursives Verständnis können definiert werden. Das schwache System RCA besteht aus der Elementarfunktionsarithmetik EFA (die grundlegenden Axiome plus die Δ Induktion auf der bereicherten Sprache mit einer Exponentialoperation) plus das Δ Verständnis. Über RCA ist rekursives Verständnis, wie definiert, früher (d. h. mit der Σ Induktion) zur Behauptung gleichwertig, dass ein Polynom (über ein zählbares Feld) nur begrenzt viele Wurzeln und zum Klassifikationslehrsatz für begrenzt erzeugte Gruppen von Abelian hat. Das System RCA hat denselben Beweis theoretische Ordnungszahl ω als EFA und ist über EFA für &Pi konservativ; Sätze.
• Das Lemma des schwachen Schwachen Königs ist die Behauptung, dass ein Subbaum des unendlichen binären Baums, der keine unendlichen Pfade hat, ein asymptotisch verschwindendes Verhältnis der Blätter ausführlich n hat (mit einer gleichförmigen Schätzung betreffs, wie viele Blätter der Länge n bestehen). Eine gleichwertige Formulierung ist, dass jede Teilmenge des Kantor-Raums, der positives Maß hat, nichtleer ist (das ist in RCA nicht nachweisbar). WWKL wird durch das Angrenzen an dieses Axiom RCA erhalten. Es ist zur Behauptung gleichwertig, dass, wenn die Einheit echter Zwischenraum durch eine Folge von Zwischenräumen dann bedeckt wird, die Summe ihrer Längen mindestens ein ist. Die Mustertheorie von WWKL wird mit der Theorie von algorithmisch Zufallsfolgen nah verbunden. Insbesondere ein ω-model von RCA befriedigt das Lemma des schwachen schwachen Königs wenn, und nur wenn für jeden Satz X es einen Satz Y gibt, der hinsichtlich X 1-zufällig ist.
• DNR (kurz für "diagonal nichtrekursiven") fügt zu RCA ein Axiom hinzu, die Existenz einer diagonal nichtrekursiven Funktion hinsichtlich jedes Satzes behauptend. D. h. DNR stellt fest, dass, für jeden Satz A, dort eine Gesamtfunktion f solch besteht, dass für den ganzen e die eth teilweise rekursive Funktion mit dem Orakel A f nicht gleich ist. DNR ist ausschließlich schwächer als WWKL (Lempp u. a. 2004).
• Δ-comprehension ist auf bestimmte arithmetischem transfinitem recursion analoge Weisen, wie rekursives Verständnis zum Lemma des schwachen Königs ist. Es hat die hyperarithmetischen Sätze als minimaler ω-model. Arithmetischer transfiniter recursion beweist Δ-comprehension, aber nicht den anderen Weg ringsherum.
• Σ-choice ist die Behauptung, dass, wenn η (n, X) eine Σ solche Formel ist, dass für jeden n dort eine X Zufriedenheit η dann besteht, es eine Folge von Sätzen X solch gibt, dass η (n, X) für jeden n hält. Σ-choice hat auch die hyperarithmetischen Sätze als minimaler ω-model. Arithmetischer transfiniter recursion beweist Σ-choice, aber nicht den anderen Weg ringsherum.

ω-models und β-models

ω in ω-model tritt für den Satz von natürlichen Zahlen (oder begrenzte Ordnungszahlen) ein. ω-model ist ein Modell für ein Bruchstück der Arithmetik der zweiten Ordnung, deren Teil der ersten Ordnung das Standardmodell der Arithmetik von Peano ist, aber dessen Teil der zweiten Ordnung umgangssprachlich sein kann. Genauer, ω-model wird durch eine Wahl S⊆2 Teilmengen &omega gegeben;. die ersten Ordnungsvariablen werden auf die übliche Weise als Elemente &omega interpretiert; und +, × haben Sie ihre üblichen Bedeutungen, während die zweiten Ordnungsvariablen als Elemente von S interpretiert werden. Es gibt einen Standard ω Modell, wo man gerade S nimmt, um aus allen Teilmengen der ganzen Zahlen zu bestehen. Jedoch gibt es auch anderen ω-models; zum Beispiel hat RCA einen minimalen ω-model, wo S aus den rekursiven Teilmengen ω. besteht

β Modell ist ω Modell, das zum Standard ω-model für &Pi gleichwertig ist; und Σ Sätze (mit Rahmen).

Non-ω Modelle sind auch besonders in den Beweisen von Bewahrungslehrsätzen nützlich.

Außenverbindungen

• Die Hausseite von Harvey Friedman
• Die Hausseite von Stephen G. Simpson