Arithmetik zweiter Ordnung - Second-order arithmetic

In der mathematischen Logik ist die Arithmetik zweiter Ordnung eine Sammlung von axiomatischen Systemen, die die natürlichen Zahlen und ihre Teilmengen formalisieren . Sie ist eine Alternative zur axiomatischen Mengenlehre als Grundlage für viele, aber nicht die gesamte Mathematik.

Ein Vorläufer der Arithmetik zweiter Ordnung, die Parameter dritter Ordnung beinhaltet, wurde von David Hilbert und Paul Bernays in ihrem Buch Grundlagen der Mathematik vorgestellt . Die Standardaxiomatisierung der Arithmetik zweiter Ordnung wird mit Z _{2 bezeichnet} .

Die Arithmetik zweiter Ordnung umfasst die Peano-Arithmetik , ist aber deutlich stärker als ihr Gegenstück erster Ordnung . Im Gegensatz zur Peano-Arithmetik ermöglicht die Arithmetik zweiter Ordnung die Quantifizierung über Mengen natürlicher Zahlen sowie über die Zahlen selbst. Da reelle Zahlen auf bekannte Weise als ( unendliche ) Mengen natürlicher Zahlen dargestellt werden können und die Arithmetik zweiter Ordnung eine Quantifizierung über solche Mengen erlaubt, ist es möglich, die reellen Zahlen in Arithmetik zweiter Ordnung zu formalisieren . Aus diesem Grund wird die Arithmetik zweiter Ordnung manchmal als „ Analyse “ bezeichnet (Sieg 2013, S. 291).

Arithmetik zweiter Ordnung kann auch als eine schwache Version der Mengenlehre angesehen werden, in der jedes Element entweder eine natürliche Zahl oder eine Menge natürlicher Zahlen ist. Obwohl sie viel schwächer als die Zermelo-Fraenkel-Mengentheorie ist , kann die Arithmetik zweiter Ordnung im Wesentlichen alle Ergebnisse der klassischen Mathematik beweisen, die in ihrer Sprache ausdrückbar sind.

Ein Subsystem der Arithmetik zweiter Ordnung ist eine Theorie in der Sprache der Arithmetik zweiter Ordnung, von der jedes Axiom ein Satz der vollständigen Arithmetik zweiter Ordnung (Z ₂ ) ist. Solche Subsysteme sind für die Umkehrmathematik unerlässlich , ein Forschungsprogramm, das untersucht, wie viel von der klassischen Mathematik in bestimmten schwachen Subsystemen unterschiedlicher Stärke abgeleitet werden kann. Ein Großteil der Kernmathematik kann in diesen schwachen Subsystemen formalisiert werden, von denen einige im Folgenden definiert werden. Die Umkehrmathematik verdeutlicht auch das Ausmaß und die Art und Weise, in der die klassische Mathematik nicht- konstruktiv ist .

Definition

Syntax

Die Sprache der Arithmetik zweiter Ordnung ist zweisortiert . Die erste Art von Begriffen und insbesondere Variablen , die normalerweise mit Kleinbuchstaben bezeichnet werden, bestehen aus Individuen , deren beabsichtigte Interpretation als natürliche Zahlen ist. Die andere Art von Variablen, die auch als „Mengenvariablen“, „Klassenvariablen“ oder sogar „Prädikate“ bezeichnet werden, werden normalerweise mit Großbuchstaben bezeichnet. Sie beziehen sich auf Klassen/Prädikate/Eigenschaften von Individuen und können daher als Mengen natürlicher Zahlen betrachtet werden. Sowohl Individuen als auch Mengenvariablen können universell oder existentiell quantifiziert werden. Eine Formel ohne gebundene Mengenvariablen (d. h. keine Quantoren über Mengenvariablen) heißt arithmetisch . Eine arithmetische Formel kann frei gesetzte Variablen und gebundene individuelle Variablen haben.

Einzelne Terme werden aus der Konstanten 0, der unären Funktion S (der Nachfolgerfunktion ) und den binären Operationen + und (Addition und Multiplikation) gebildet. Die Nachfolgerfunktion addiert 1 zu ihrer Eingabe. Die Relationen = (Gleichheit) und < (Vergleich natürlicher Zahlen) beziehen sich auf zwei Individuen, während die Relation ∈ (Zugehörigkeit) ein Individuum und eine Menge (oder Klasse) in Beziehung setzt. In der Notation ist also die Sprache der Arithmetik zweiter Ordnung durch die Signatur gegeben . ${\displaystyle \cdot}$${\displaystyle {\mathcal{L}}=\{0,S,+,\cdot,=,<,\in\}}$

Zum Beispiel ist , eine wohlgeformte Formel der Arithmetik zweiter Ordnung, die arithmetisch ist, eine freie Mengenvariable X und eine gebundene individuelle Variable n hat (aber keine gebundenen Mengenvariablen, wie es von einer arithmetischen Formel verlangt wird ) – während a wohlgeformte Formel, die nicht arithmetisch ist und eine gebundene Mengenvariable X und eine gebundene individuelle Variable n hat . ${\displaystyle \forall n(n\in X\rightarrow Sn\in X)}$${\displaystyle \exists X\forall n(n\in X\leftrightarrow n<SSSSSS0\cdot SSSSSSS0)}$

Semantik

Mehrere verschiedene Interpretationen der Quantoren sind möglich. Wenn die Arithmetik zweiter Ordnung unter Verwendung der vollständigen Semantik der Logik zweiter Ordnung untersucht wird, erstrecken sich die Mengenquantoren über alle Teilmengen des Bereichs der Zahlenvariablen. Wenn die Arithmetik zweiter Ordnung unter Verwendung der Semantik der Logik erster Ordnung (Henkin-Semantik) formalisiert wird, dann enthält jedes Modell eine Domäne für die Mengenvariablen, über die sie sich erstrecken können, und diese Domäne kann eine echte Teilmenge der vollständigen Potenzmenge des Zahlenbereichs sein Variablen (Shapiro 1991, S. 74–75).

Axiome

Basic

Die folgenden Axiome werden als grundlegende Axiome oder manchmal als Robinson-Axiome bezeichnet. Die resultierende Theorie erster Ordnung , bekannt als Robinson-Arithmetik , ist im Wesentlichen Peano-Arithmetik ohne Induktion. Der Diskursbereich für die quantifizierten Variablen sind die natürlichen Zahlen , die kollektiv mit N bezeichnet werden und das ausgezeichnete Mitglied " Null " enthalten. ${\displaystyle \ 0}$

Die primitiven Funktionen sind die unäre Nachfolgerfunktion , bezeichnet durch Präfix , und zwei binäre Operationen , Addition und Multiplikation , bezeichnet durch Infix " + " bzw. " " . Es gibt auch eine primitive binäre Beziehung namens order , die mit dem Infix "<" bezeichnet wird. ${\displaystyle S}$${\displaystyle \cdot}$

Axiome, die die Nachfolgerfunktion und die Null bestimmen :

1. („der Nachfolger einer natürlichen Zahl ist nie null“)${\displaystyle \forall m[Sm=0\rightarrow\bot].}$

2. („die Nachfolgerfunktion ist injektiv “)${\displaystyle \forall m\forall n[Sm=Sn\rightarrow m=n].}$

3. („jede natürliche Zahl ist Null oder ein Nachfolger“)${\displaystyle \forall n[0=n\lor \exists m[Sm=n]].}$

Rekursiv definierter Zusatz :

4. ${\displaystyle \forall m[m+0=m].}$

5. ${\displaystyle \forall m\forall n[m+Sn=S(m+n)].}$

Multiplikation rekursiv definiert:

6. ${\displaystyle \forall m[m\cdot 0=0].}$

7. ${\displaystyle \forall m\forall n[m\cdot Sn=(m\cdot n)+m].}$

Axiome zur Ordnungsrelation "<":

8. („keine natürliche Zahl ist kleiner als Null“)${\displaystyle \forall m[m<0\rightarrow\bot].}$

9. ${\displaystyle \forall n\forall m[m<Sn\leftrightarrow (m<n\lor m=n)].}$

10. („jede natürliche Zahl ist null oder größer null“)${\displaystyle \forall n[0=n\lor 0<n].}$

11. ${\displaystyle \forall m\forall n[(Sm<n\lor Sm=n)\leftrightarrow m<n].}$

Diese Axiome sind alle Aussagen erster Ordnung . Das heißt, alle Variablen erstrecken sich über die natürlichen Zahlen und nicht über Mengen davon, eine Tatsache, die noch stärker ist als ihre Arithmetik. Darüber hinaus gibt es in Axiom 3 nur einen existenziellen Quantor . Die Axiome 1 und 2 bilden zusammen mit einem Axiomenschema der Induktion die übliche Peano-Dedekind- Definition von N . Wenn man diesen Axiomen ein beliebiges Axiomenschema der Induktion hinzufügt, werden die Axiome 3, 10 und 11 überflüssig.

Induktions- und Verständnisschema

Ist φ( n ) eine Formel der Arithmetik zweiter Ordnung mit einer freien Zahlenvariablen n und möglichen weiteren freien Zahlen- oder Mengenvariablen (geschrieben m _• und X _• ), dann ist das Induktionsaxiom für φ das Axiom:

${\displaystyle \forall m\forall X((\varphi (0)\land \forall n(\varphi (n)\rightarrow \varphi (Sn)))\rightarrow \forall n\varphi (n))}$

Das ( vollständige ) Induktionsschema zweiter Ordnung besteht aus allen Instanzen dieses Axioms über alle Formeln zweiter Ordnung.

Eine besonders wichtige Instanz des Induktionsschemas ist, wenn φ die Formel “ ” ist, die die Tatsache ausdrückt, dass n ein Mitglied von X ist ( X ist eine freie Mengenvariable): In diesem Fall ist das Induktionsaxiom für φ ${\displaystyle n\in X}$

${\displaystyle \forall X((0\in X\land \forall n(n\in X\rightarrow Sn\in X))\rightarrow \forall n(n\in X))}$

Dieser Satz heißt Induktionsaxiom zweiter Ordnung .

Wenn φ( n ) eine Formel mit einer freien Variablen n und möglicherweise anderen freien Variablen, aber nicht der Variablen Z ist , ist das Verständnisaxiom für φ die Formel

${\displaystyle \exists Z\forall n(n\in Z\leftrightarrow\varphi(n))}$

Dieses Axiom ermöglicht es, die Menge der natürlichen Zahlen zu bilden, die φ( n ) erfüllen . Es gibt eine technische Einschränkung, dass die Formel φ die Variable Z nicht enthalten darf , denn sonst würde die Formel zum Verständnisaxiom führen ${\displaystyle Z=\{n|\varphi(n)\}}$${\displaystyle n\not\in Z}$

${\displaystyle \exists Z\forall n(n\in Z\leftrightarrow n\not \in Z)}$,

was inkonsistent ist. Im Rest dieses Artikels wird von dieser Konvention ausgegangen.

Das komplette System

Die formale Theorie der Arithmetik zweiter Ordnung (in der Sprache der Arithmetik zweiter Ordnung) besteht aus den Grundaxiomen, dem Verständnisaxiom für jede Formel φ (arithmetisch oder anders) und dem Induktionsaxiom zweiter Ordnung. Diese Theorie wird manchmal als vollständige Arithmetik zweiter Ordnung bezeichnet , um sie von ihren unten definierten Subsystemen zu unterscheiden. Da eine vollständige Semantik zweiter Ordnung impliziert, dass jede mögliche Menge existiert, können die Verständnisaxiome als Teil des deduktiven Systems angesehen werden, wenn diese Semantik verwendet wird (Shapiro 1991, S. 66).

Modelle

Dieser Abschnitt beschreibt Arithmetik zweiter Ordnung mit Semantik erster Ordnung. So besteht ein Modell der Sprache der Arithmetik zweiter Ordnung aus einer Menge M (die den Bereich der einzelnen Variablen bildet) zusammen mit einer Konstanten 0 (einem Element von M ), einer Funktion S von M nach M , zwei binären Operationen + und · auf M , eine binäre Relation < auf M , und eine Sammlung D von Teilmengen von M , die der Bereich der Mengenvariablen ist. Das Weglassen von D erzeugt ein Modell der Sprache der Arithmetik erster Ordnung. ${\displaystyle {\mathcal{M}}}$

Wenn D die volle Potenz von M ist , wird das Modell als vollständiges Modell bezeichnet . Die Verwendung der vollständigen Semantik zweiter Ordnung ist gleichbedeutend mit der Beschränkung der Modelle der Arithmetik zweiter Ordnung auf die vollständigen Modelle. Tatsächlich haben die Axiome der Arithmetik zweiter Ordnung nur ein vollständiges Modell. Dies folgt daraus, dass die Axiome der Peano-Arithmetik mit dem Induktionsaxiom zweiter Ordnung nur ein Modell unter Semantik zweiter Ordnung haben. ${\displaystyle {\mathcal{M}}}$

Wenn M die übliche Menge natürlicher Zahlen mit ihren üblichen Operationen ist, heißt das ω-Modell . In diesem Fall kann das Modell mit D identifiziert werden , seiner Sammlung von Mengen von Naturwerten, da diese Menge ausreicht, um ein -Modell vollständig zu bestimmen. ${\displaystyle {\mathcal{M}}}$

Das einzigartige vollständige -Modell, das die übliche Menge natürlicher Zahlen mit ihrer üblichen Struktur und all ihren Teilmengen ist, wird das beabsichtigte oder Standardmodell der Arithmetik zweiter Ordnung genannt. ${\displaystyle\omega}$

Definierbare Funktionen

Die in der Arithmetik zweiter Ordnung beweisbar totalen Funktionen erster Ordnung sind genau dieselben wie die im System F darstellbaren (Girard und Taylor 1987, S. 122–123). Fast äquivalent ist System F die Theorie der Funktionale, die der Arithmetik zweiter Ordnung entsprechen, ähnlich wie Gödels System T der Arithmetik erster Ordnung in der Dialectica-Interpretation entspricht .

Subsysteme

Es gibt viele benannte Subsysteme der Arithmetik zweiter Ordnung.

Eine tiefgestellte 0 im Namen eines Subsystems zeigt an, dass es nur einen eingeschränkten Teil des vollständigen Induktionsschemas zweiter Ordnung enthält (Friedman 1976). Eine solche Einschränkung verringert die beweistheoretische Stärke des Systems erheblich. Zum Beispiel ist das unten beschriebene System ACA ₀ mit der Peano-Arithmetik äquikonsistent . Die entsprechende Theorie ACA, bestehend aus ACA ₀ plus dem vollständigen Induktionsschema zweiter Ordnung, ist stärker als die Peano-Arithmetik.

Rechenverständnis

Viele der gut untersuchten Subsysteme beziehen sich auf die Verschlusseigenschaften von Modellen. Zum Beispiel kann gezeigt werden, dass jedes ω-Modell der vollständigen Arithmetik zweiter Ordnung unter Turing-Sprung abgeschlossen ist , aber nicht jedes unter Turing-Sprung abgeschlossene ω-Modell ist ein Modell der vollständigen Arithmetik zweiter Ordnung. Das Subsystem ACA ₀ enthält gerade genug Axiome, um den Begriff der Schließung unter dem Turing-Sprung zu erfassen.

ACA ₀ ist definiert als die Theorie bestehend aus den Grundaxiomen, dem arithmetischen Verständnis-Axiom- Schema (also dem Verständnis-Axiom für jede arithmetische Formel φ) und dem gewöhnlichen Induktionsaxiom zweiter Ordnung. Es wäre äquivalent, das gesamte arithmetische Induktionsaxiomenschema einzubeziehen, also das Induktionsaxiom für jede arithmetische Formel φ einzubeziehen.

Es kann gezeigt werden, dass eine Sammlung S von Teilmengen von ω genau dann ein ω-Modell von ACA _{0 bestimmt,} wenn S unter Turing-Sprung, Turing-Reduzierbarkeit und Turing-Join abgeschlossen ist (Simpson 2009, S. 311–313).

Der Index 0 in ACA ₀ zeigt an, dass nicht jede Instanz des Induktionsaxiomenschemas in diesem Subsystem enthalten ist. Für ω-Modelle, die automatisch jede Instanz des Induktionsaxioms erfüllen, macht dies keinen Unterschied. Es ist jedoch bei der Untersuchung von Nicht-ω-Modellen von Bedeutung. Das System bestehend aus ACA ₀ plus Induktion für alle Formeln wird manchmal als ACA ohne Index bezeichnet.

Das System ACA ₀ ist eine konservative Erweiterung der Arithmetik erster Ordnung (bzw andernfalls) in der Sprache der Arithmetik erster Ordnung (die überhaupt keine Klassenvariablen zulässt). Insbesondere hat sie wegen des begrenzten Induktionsschemas die gleiche beweistheoretische Ordinalzahl ε ₀ wie die Arithmetik erster Ordnung.

Die arithmetische Hierarchie für Formeln

Eine Formel heißt beschränkt arithmetisch oder Δ ⁰ ₀ , wenn alle ihre Quantoren die Form ∀ n < t oder ∃ n < t haben (wobei n die zu quantifizierende individuelle Variable und t ein einzelner Term ist), wobei

${\displaystyle \forall n<t(\cdots)}$

steht für

${\displaystyle \forall n(n<t\rightarrow\cdots)}$

und

${\displaystyle \exists n<t(\cdots)}$

steht für

${\displaystyle \exists n(n<t\land\cdots)}$.

Eine Formel heißt Σ ⁰ ₁ (oder manchmal Σ ₁ ), bzw. Π ⁰ ₁ (oder manchmal Π ₁ ), wenn sie die Form ∃ m _• (φ), bzw. ∀ m _• (φ) hat, wobei φ eine beschränkte arithmetische Formel ist und m ist eine individuelle Variable (die in φ frei ist). Allgemeiner heißt eine Formel Σ ⁰ _n bzw. Π ⁰ _n, wenn sie durch Addition existenzieller bzw. universeller Einzelquantoren zu einer Π ⁰ _{n −1} bzw. Σ ⁰ _{n −1} Formel (und Σ ⁰ ₀ und Π ⁰ ₀ sind alle äquivalent zu Δ ⁰ ₀ ). Durch Konstruktion sind alle diese Formeln arithmetisch (keine Klassenvariablen sind jemals gebunden) und tatsächlich kann man sehen, dass jede arithmetische Formel einer Σ ⁰ _n oder Π ⁰ _n Formel für alle äquivalent ist , wenn man die Formel in die Skolem-Pränexform bringt groß genug , um n .

Rekursives Verstehen

Das Subsystem RCA ₀ ist ein schwächeres System als ACA ₀ und wird oft als Basissystem in der umgekehrten Mathematik verwendet . Es besteht aus: den Grundaxiomen, dem Σ ⁰ ₁ Induktionsschema und dem Δ ⁰ ₁ Verständnisschema. Der erstere Term ist klar: Das Σ ⁰ ₁ Induktionsschema ist das Induktionsaxiom für jede Σ ⁰ ₁ Formel φ. Der Begriff „Δ ⁰ ₁ Verständnis“ ist komplexer, da es keine Δ ⁰ ₁ Formel gibt. Das ⁰ _1- Verständnisschema behauptet stattdessen das Verständnisaxiom für jede Σ ⁰ _1- Formel, die einer Π ⁰ _1- Formel äquivalent ist . Dieses Schema beinhaltet für jede Σ ⁰ ₁ Formel φ und jede Π ⁰ ₁ Formel ψ das Axiom:

${\displaystyle \forall m\forall X((\forall n(\varphi (n)\leftrightarrow \psi (n)))\rightarrow \exists Z\forall n(n\in Z\leftrightarrow \varphi (n)) )}$

Die Folge erster Ordnung von RCA ₀ ist die gleiche wie die des Subsystems IΣ ₁ der Peano-Arithmetik, in der die Induktion auf Σ ⁰ ₁ Formeln beschränkt ist. IΣ _{1 wiederum} ist konservativ gegenüber primitiver rekursiver Arithmetik (PRA) für Sätze. Außerdem ist die beweistheoretische Ordinalzahl von ω ^ω , die gleiche wie die von PRA. ${\displaystyle \Pi_{2}^{0}}$${\displaystyle \mathrm {RCA} _{0}}$

Es ist ersichtlich, dass eine Sammlung S von Teilmengen von ω genau dann ein ω-Modell von RCA _{0 bestimmt,} wenn S unter Turing-Reduzierbarkeit und Turing-Join abgeschlossen ist. Insbesondere ergibt die Sammlung aller berechenbaren Teilmengen von ω ein ω-Modell von RCA ₀ . Dies ist die Motivation hinter dem Namen dieses Systems – wenn die Existenz einer Menge mit RCA _{0 nachgewiesen werden kann} , dann ist die Menge rekursiv (dh berechenbar).

Schwächere Systeme

Manchmal wird ein noch schwächeres System als Cinch ₀ gewünscht. Ein solches System ist wie folgt definiert: Man muss zuerst die Sprache der Arithmetik um eine Exponentialfunktion erweitern (in stärkeren Systemen kann die Exponentialfunktion durch den üblichen Trick durch Addition und Multiplikation definiert werden, aber wenn das System zu schwach wird, ist dies kein länger möglich) und die grundlegenden Axiome durch die offensichtlichen Axiome, die die Exponentiation induktiv aus der Multiplikation definieren; dann besteht das System aus den (angereicherten) Grundaxiomen plus Δ ⁰ ₁ Verständnis, plus Δ ⁰ ₀ Induktion.

Stärkere Systeme

Über ACA ₀ ist jede Formel der Arithmetik zweiter Ordnung äquivalent zu einer ¹ _n oder Π ¹ _n Formel für alle groß genug n . Das System Π ¹ ₁ -Verständnis ist das System bestehend aus den Grundaxiomen , plus dem gewöhnlichen Induktionsaxiom zweiter Ordnung und dem Verständnisaxiom für jede Π ¹ ₁ Formel φ. Dies entspricht ¹ ₁ -Verständnis (dagegen ist Δ ¹ ₁ -Verständnis, analog zu Δ ⁰ ₁ -Verständnis definiert, schwächer).

Projektive Determiniertheit

Projektive Determiniertheit ist die Behauptung, dass jedes perfekte Informationsspiel für zwei Spieler mit ganzen Zügen, Spiellänge ω und projektivem Auszahlungssatz bestimmt ist, dh dass einer der Spieler eine Gewinnstrategie hat. (Der erste Spieler gewinnt das Spiel, wenn das Spiel zur Auszahlungsmenge gehört; andernfalls gewinnt der zweite Spieler.) Eine Menge ist projektiv, wenn (als Prädikat) sie durch eine Formel in der Sprache der Arithmetik zweiter Ordnung ausdrückbar ist reelle Zahlen als Parameter, so dass projektive Bestimmtheit als Schema in der Sprache von Z ₂ ausdrückbar ist .

Viele natürliche Aussagen, die in der Sprache der Arithmetik zweiter Ordnung ausdrückbar sind, sind unabhängig von Z ₂ und sogar ZFC, aber aus projektiver Bestimmtheit beweisbar. Beispiele sind koanalytische perfekte Teilmengeneigenschaft , Messbarkeit und die Eigenschaft von Baire für Mengen, Uniformisierung usw. Über eine schwache Basistheorie (wie RCA ₀ ) impliziert die projektive Determination Verständnis und liefert eine im Wesentlichen vollständige Theorie der Arithmetik zweiter Ordnung – natürliche Aussagen in der Sprache von Z ₂ sind von Z ₂ unabhängige mit projektiver Determiniertheit schwer zu finden (Woodin 2001). ${\displaystyle \Sigma_{2}^{1}}$${\displaystyle \Pi_{3}^{1}}$

ZFC + {gibt es n cardinals Woodin : n ist eine natürliche Zahl} über Z konservativ ₂ mit projektiven Determination, dass eine Aussage in der Sprache der zweiten Ordnung Arithmetik beweisbar in Z ₂ mit projektiven Determination iff seiner Übersetzung in die Sprache der Mengenlehre ist beweisbar in ZFC + {es gibt n Woodin-Kardinäle: n ∈N}.

Mathematik codieren

Arithmetik zweiter Ordnung formalisiert natürliche Zahlen und Mengen natürlicher Zahlen direkt. Es ist jedoch in der Lage, andere mathematische Objekte indirekt über Kodierungstechniken zu formalisieren, eine Tatsache, die erstmals von Weyl (Simpson 2009, S. 16) bemerkt wurde. Die ganzen Zahlen, rationalen Zahlen und reellen Zahlen können alle im Subsystem RCA ₀ formalisiert werden , zusammen mit vollständigen separierbaren metrischen Räumen und stetigen Funktionen zwischen ihnen (Simpson 2009, Kapitel II).

Das Forschungsprogramm Reverse Mathematics verwendet diese Formalisierungen der Mathematik in der Arithmetik zweiter Ordnung, um die zum Beweis mathematischer Theoreme erforderlichen Mengen-Existenz-Axiome zu untersuchen (Simpson 2009, S. 32). Beispielsweise ist der Zwischenwertsatz für Funktionen von den reellen zu den reellen Zahlen in RCA ₀ beweisbar (Simpson 2009, S. 87), während der Satz von Bozen – Weierstrass äquivalent zu ACA ₀ über RCA _{0 ist} (Simpson 2009, S. 34 .). ).

Die obige Codierung funktioniert gut für stetige und totale Funktionen, wie in (Kohlenbach 2002, Abschnitt 4) gezeigt, unter der Annahme einer Basistheorie höherer Ordnung plus schwachem Koenig-Lemma . Wie vielleicht erwartet, ist die Codierung im Fall der Topologie oder der Maßtheorie nicht unproblematisch, wie z. B. in (Hunter, 2008) oder (Normann-Sanders, 2019) untersucht wurde. Allerdings führt selbst die Codierung von Riemann-integrierbaren Funktionen zu Problemen: Wie in (Normann-Sanders, 2020) gezeigt, sind die minimalen (Verständnis-)Axiome, die benötigt werden, um Arzelàs Konvergenzsatz für das Riemann-Integral zu beweisen, *sehr* unterschiedlich, je nachdem, ob man zweite- Bestellcodes oder Funktionen dritter Ordnung.

Siehe auch

• Paris-Harrington-Theorem
• Presburger Arithmetik
• Wahre Arithmetik

Verweise

• Burgess, JP (2005), Fixing Frege , Princeton University Press.
• Buss, SR (1998), Handbuch der Beweistheorie , Elsevier. ISBN  0-444-89840-9
• Friedman, H. (1976), "Systeme der Arithmetik zweiter Ordnung mit eingeschränkter Induktion", I, II (Abstracts). Journal of Symbolic Logic , V. 41, S. 557– 559. JStor
• Girard, L. und Taylor (1987), Beweise und Typen , Cambridge University Press.
• Hilbert, D. und Bernays, P. (1934), Grundlagen der Mathematik , Springer-Verlag. MR 0237246
• Hunter, James, Reverse Topology höherer Ordnung , Dissertation, University of Madison-Wisconsin [1] .
• Kohlenbach, U. , Grundlegende und mathematische Verwendungen höherer Typen , Überlegungen zu den Grundlagen der Mathematik, Lect. Anmerkungen Log., vol. 15, ASL, 2002, S. 92–116.
• Dag Normann und Sam Sanders, Darstellungen in der Maßtheorie , arXiv: 1902.02756 , (2019).
• Dag Normann und Sam Sanders, On the uncountability of $\mathbb{R}$ , arxiv: [2] , (2020), S. 37.
• Sieg, W. (2013), Hilberts Programme and Beyond , Oxford University Press.
• Shapiro, S. (1991), Stiftungen ohne Fundamentalismus , Oxford University Press. ISBN  0-19-825029-0
• Simpson, SG (2009), Subsystems of Second Order Arithmetic , 2. Auflage, Perspectives in Logic, Cambridge University Press. ISBN  978-0-521-88439-6 MR 2517689
• Takeuti, G. (1975) Beweistheorie ISBN  0-444-10492-5
• Woodin, WH (2001), „Die Kontinuumshypothese, Teil I“, Mitteilungen der American Mathematical Society , v. 48 n. 6.