Ordinal analys

I bevisteorin tilldelar ordinalanalys ordinaler (ofta stora räknebara ordinaler ) till matematiska teorier som ett mått på deras styrka. Om teorier har samma bevisteoretiska ordinal är de ofta ekvikonsistenta , och om en teori har en större bevisteoretisk ordinal än en annan kan det ofta bevisa överensstämmelsen hos den andra teorin.

Historia

Fältet för ordinalanalys bildades när Gerhard Gentzen 1934 använde cut-eliminering för att bevisa, i moderna termer, att den bevisteoretiska ordinalen för Peano-aritmetiken är ε ₀ . Se Gentzens konsistensbevis .

Definition

Ordinalanalys avser sanna, effektiva (rekursiva) teorier som kan tolka en tillräcklig del av aritmetiken för att göra påståenden om ordinalnotationer.

Den bevisteoretiska ordinalen för en sådan teori $T$ är det högsta av ordningstyperna för alla ordningsnotationer (nödvändigtvis rekursiva , se nästa avsnitt) som teorin kan bevisa är välgrundade — det högsta av alla ordningstal ${ \displaystyle \alpha }$ för vilken det finns en notation $o$ i Kleenes mening så att $T$ bevisar att $o$ är en ordningsnotation. På motsvarande sätt är det supremum av alla ordinaler $\alpha$ så att det finns en rekursiv relation $R$ på $\omega$ (mängden naturliga tal) som välordnar den med ordinal $\alpha$ och så att $T$ bevisar transfinit induktion av aritmetiska satser för $R$ .

Ordinalnotationer

Vissa teorier, såsom subsystem av andra ordningens aritmetik, har ingen konceptualisering av eller sätt att föra argument om transfinita ordningstal. Till exempel, för att formalisera vad det betyder för ett delsystem av Z ₂ $T$ att "visa $\alpha$ välordnad", konstruerar vi istället en ordningsnotation $(A,{\tilde {<}})$ med ordertyp $\alpha$ . $T$ kan nu arbeta med olika transfinita induktionsprinciper längs ${\displaystyle (A,{\tilde {<}})} ,$ som ersätter resonemang om mängdteoretiska ordinaler.

Det finns dock vissa patologiska notationssystem som är oväntat svåra att arbeta med. Till exempel ger Rathjen ett primitivt rekursivt notationssystem $(\mathbb {N} ,<_{T})$ som är välgrundat om PA är konsekvent, trots att det har ordningstyp ${\ displaystyle \omega }$ - att inkludera en sådan notation i ordningsanalysen av PA skulle resultera i den falska likheten ${\mathsf {PTO(PA)}}=\omega$ .

Övre gräns

För varje teori som är både $\Sigma _{1}^{1}$ -axiomatiserbar och $\Pi _{1}^{1}$ -ljud, förekomsten av ett rekursivt att beställa att teorin inte kan bevisa är välordnad följer av $\Sigma _{1}^{1}$ begränsningssatsen, och nämnda bevisligen välgrundade ordningsnotationer är i själva verket välgrundade av $\Pi _{1}^{1}$ -ljud. Således kommer den bevisteoretiska ordinalen för en $\Pi _{1}^{1}$ -ljudteori som har en $\Sigma _{1}^{1}$ axiomatisering alltid vara en (räknebar) rekursiv ordinal , det vill säga mindre än Church–Kleene ordinal $\omega _{1}^{\mathrm {CK} }$ .

Exempel

Teorier med bevisteoretisk ordinal ω

• Q, Robinson aritmetik (även om definitionen av den bevisteoretiska ordinalen för sådana svaga teorier måste justeras) [ .
• PA ^– , första ordningens teori om den icke-negativa delen av en diskret ordnad ring.

Teorier med bevisteoretisk ordinal ω ²

• RFA, rudimentär funktionsaritmetik .
• ₀₀ IΔ , aritmetik med induktion på Δ -predikat utan något axiom som hävdar att exponentieringen är total.

Teorier med bevisteoretisk ordinal ω ³

• EFA, elementär funktionsaritmetik .
• ₀₀ IΔ + exp, aritmetik med induktion på Δ -predikat utökade med ett axiom som hävdar att exponentieringen är total.
• RCA ^*
  ₀ , en andra ordningens form av EFA som ibland används i omvänd matematik .
• WKL ^*
  ₀ , en andra ordningens form av EFA som ibland används i omvänd matematik .

Friedmans stora gissningar antyder att mycket "vanlig" matematik kan bevisas i svaga system som har detta som sin bevisteoretiska ordinal.

Teorier med bevisteoretisk ordinal ω ⁿ (för n = 2, 3, ... ω)

• ₀ IΔ eller EFA förstärkt med ett axiom som säkerställer att varje element i den n -:e nivån ${\mathcal {E}}^{n}$ i Grzegorczyk-hierarkin är total.

Teorier med bevisteoretisk ordinal ω ^ω

• ₀ RCA , rekursiv förståelse .
• ₀ WKL , svaga Königs lemma .
• PRA, primitiv rekursiv aritmetik .
• IΣ ₁ , aritmetik med induktion på Σ ₁ -predikat.

Teorier med bevisteoretisk ordinal ε₀

• PA, Peano aritmetik ( visas av Gentzen med cut elimination ).
• ₀ ACA , aritmetisk förståelse .

Teorier med bevisteoretisk ordinal Feferman–Schütte ordinal Γ ₀

• ₀ ATR , aritmetisk transfinit rekursion .
• Martin-Löf typteori med godtyckligt många universum på ändliga nivåer.

Denna ordinal anses ibland vara den övre gränsen för "predikativa" teorier.

Teorier med bevisteoretisk ordinal Bachmann-Howard ordinal

• ID ₁ , den första teorin om induktiva definitioner .
• KP, Kripke–Platek mängdlära med oändlighetens axiom .
• CZF, Aczels konstruktiva Zermelo–Fraenkel-mängdteori .
• ₀ EON, en svag variant av Fefermans explicita matematiksystem T .

Kripke-Platek- eller CZF-mängdteorierna är svaga mängdteorier utan axiom för den fulla kraftmängden som ges som uppsättning av alla delmängder. Istället tenderar de att antingen ha axiom för begränsad separation och bildande av nya mängder, eller så tillåter de existensen av vissa funktionsrum (exponentiering) istället för att skära ut dem från större relationer.

Teorier med större bevisteoretiska ordtal

Olöst problem i matematik :

Vad är den bevisteoretiska ordinalen för full andra ordningens aritmetik?

(fler olösta problem i matematik)

• $\Pi _{1}^{1}{\mbox{-}}{\mathsf {CA}}_{0}$ , Π ₁ ¹ förståelse har en ganska stor bevisteoretik ordinal, som beskrevs av Takeuti i termer av "ordningsdiagram", och som avgränsas av ₀ ψ (Ω _ω ) i Buchholz notation . Det är också ordningen för ${\displaystyle ID_{<\omega }} ,$ teorin om ändligt itererade induktiva definitioner. Och även ordinalen för MLW, Martin-Löf typteori med indexerade W-Types Setzer (2004) .
• ID _ω , teorin om ω-itererade induktiva definitioner . Dess bevisteoretiska ordinal är lika med Takeuti-Feferman-Buchholz ordinal .
• ₀ T , Fefermans konstruktiva system av explicit matematik har en större bevisteoretisk ordinal, som också är den bevisteoretiska ordinalen för KPi, Kripke–Platek mängdlära med itererade tillåtna värden och Σ 2 1 $\ Sigma _{2}^{1}{\mbox{-}}{\mathsf {AC}}+{\mathsf {BI}}}$ .
• KPi, en förlängning av Kripke–Platek mängdteorin baserad på en rekursivt otillgänglig ordinal , har en mycket stor bevisteoretisk ordinal $\psi (\varepsilon _{I+1})$ beskriven i en tidning från 1983 av Jäger och Pohlers, där I är den minsta otillgängliga. Denna ordinal är också den bevisteoretiska ordinalen för $\Delta _{2}^{1}{\mbox{-}}{\mathsf {CA}}+{\mathsf {BI}}$ .
• KPM, en förlängning av Kripke–Platek mängdteorin baserad på en rekursivt Mahlo-ordinal , har en mycket stor bevisteoretisk ordinal θ, vilket beskrevs av Rathjen (1990) .
• MLM, en förlängning av Martin-Löfs typteori med ett Mahlo-universum, har en ännu större bevisteoretisk ordinal ψ _{Ω 1} (Ω _{M + ω )} .
• ${\mathsf {KP}}+\Pi _{3}-Ref$ har en bevisteoretisk ordinal lika med $\Psi ( \varepsilon _{K+1})$ , där $K$ refererar till den första svagt kompakta, med Rathjens Psi-funktion
• ${\mathsf {KP}}+\Pi _{\omega }-Ref$ har en bevisteoretisk ordinal lika med $\Psi _ {X}^{\varepsilon _{\Xi +1}}$ , där $\Xi$ refererar till den första $\Pi _{0}^{2}$ -obeskrivbar och ${\displaystyle \mathbb {X} =(\omega ^{+};P_{0};\epsilon ,\epsilon ,0)} ,$ med Stegerts Psi-funktion.
• $\displaystyle {\mathsf {Stabilitet}}}$ har en bevisteoretisk ordinal lika med $\Psi _{\mathbb {X} }^{\ varepsilon _{\Upsilon +1}}$ där $\Upsilon$ är en kardinalanalog av den minsta ordinalen $\alpha$ som är $\alpha +\beta$ -stabil för alla $\beta <\alpha$ och $\mathbb {X} =(\omega ^{+};P_{0};\ epsilon ,\epsilon ,0)$ , med Stegerts Psi-funktion.

De flesta teorier som kan beskriva maktmängden för de naturliga talen har bevisteoretiska ordinaler som är så stora att ingen explicit kombinatorisk beskrivning ännu har getts. Detta inkluderar $\Pi _{2}^{1}-CA_{0}$ , full andra ordningens aritmetik ( $\Pi _{\infty } ^{1}-CA_{0}$ ) och uppsättningsteorier med kraftuppsättningar inklusive ZF och ZFC. Styrkan hos intuitionistisk ZF (IZF) är lika med ZF.

Tabell över ordinalanalyser

Tabell över bevisteoretiska ordtal

Ordinal	Första ordningens aritmetik	Andra ordningens aritmetik	Kripke-Platek mängdlära	Typteori	Konstruktiv mängdlära	Explicit matematik
$\omega$	${\mathsf {Q}}$ , ${\mathsf {PA}}^{-}$
$\omega ^{2}$	${\mathsf {RFA}}$ , ${\mathsf {I\Delta }}_{0}$
$\omega ^{3}$	${\mathsf {EFA}}$ , ${\mathsf {I\Delta }}_{0}^{\mathsf {+}}$	${\mathsf {RCA}}_{0}^{*}$ , ${\mathsf {WKL}}_{0}^{*}$
$\omega ^{n}$	${\mathsf {EFA}}^{\mathsf {n}}$ , ${\mathsf {I\Delta }}_{0}^{\mathsf {n+ }}$
$\omega ^{\omega }$	${\mathsf {PRA}}$ , ${\mathsf {I\Sigma }}_{1}$	${\mathsf {RCA}}_{0}$ , ${\mathsf {WKL}}_{0}$		${\mathsf {CPRC}}$
$\varepsilon _{0}$	${\mathsf {PA}}$	${\mathsf {ACA}}_{0}$ , ${\mathsf {\Delta }}_{1}^{1}{\mathsf {-CA }}_{0}$ , ${\mathsf {\Sigma }}_{1}^{1}{\mathsf {-AC}}_{0}$				${\mathsf {EM}}_{0}$
$\varepsilon _{\varepsilon _{0}}$		${\mathsf {ACA}}$
$\varphi (\omega ,0)$	${\mathsf {ID}}_{1}\#$	${\mathsf {\Delta }}_{1}^{1}{\mathsf {-CR}}$				${\mathsf {EM}}_{0}{\mathsf {+JR}}$
$\varphi (\varepsilon _{0},0)$	${\widehat {\mathsf {ID}}}_{1}$	${\mathsf {\Delta }}_{1}^{1}{\mathsf {-CA}}$ , ${\mathsf {\Sigma }}_{1}^{1}{\mathsf {-AC}}$		${\mathsf {ML}}_{1}$		${\mathsf {EM}}_{0}{\mathsf {+J}}$
$\varphi ({\mathsf {<}}\Omega ,0)$	${\mathsf {Aut(ID\#)}}$
$\Gamma _{0}$	${\widehat {\mathsf {ID}}}_{<\omega }$ , ${\mathsf {U(PA)}}$	${\mathsf {ATR}}_{0}$ , ${\mathsf {\Delta }}_{1}^{1}{\mathsf {-CA+BR}}$	${\mathsf {KPi}}^{0}$	${\mathsf {ML}}_{<\omega }$ , ${\mathsf {MLU}}$
$\Gamma _{\omega }$			${\mathsf {KPI}}^{0}{\mathsf {+\Sigma _{1}-I}}_{\omega }$
$\Gamma _{\varepsilon _{0}}$	${\widehat {\mathsf {ID}}}_{\omega }$	${\mathsf {ATR}}$	${\mathsf {KPI}}^{0}{\mathsf {+FI}}_{\omega }$
$\varphi (1,\omega ,0)$	${\widehat {\mathsf {ID}}}_{<\omega ^{\omega }}$	${\mathsf {ATR}}_{0}+({\mathsf {\Sigma }}_{1}^{1}{\mathsf {-DC }})$	${\mathsf {KPi}}^{0}{\mathsf {+\Sigma _{1}-I}}_{\omega }$
$\varphi (1,\varepsilon _{0},0)$	${\widehat {\mathsf {ID}}}_{<\varepsilon _{0}}$	${\mathsf {ATR}}+({\mathsf {\Sigma }}_{1}^{1}{\mathsf {-DC}})$	${\mathsf {KPi}}^{0}{\mathsf {+FI}}_{\omega }$
$\varphi (1,\Gamma _{0},0)$	${\widehat {\mathsf {ID}}}_{<\Gamma _{0}}$			${\mathsf {MLS}}$
$\varphi (2,0,0)$	${\mathsf {Aut({\widehat {ID}})}}$		${\mathsf {KPh}}^{0}$	${\mathsf {Aut(ML)}}$
$\varphi (\omega ,0,0)$			${\mathsf {KPM}}^{0}$
$\psi _{0}(\Omega _{2})$	${\mathsf {ID}}_{1}$		${\mathsf {KP}}$ , ${\mathsf {KP\omega }}$	${\mathsf {ML}}_{1}{\mathsf {V}}$	${\mathsf {CZF}}$	${\mathsf {EON}}$
$\psi _{0}(\Gamma _{\Omega +1})$	${\mathsf {U(ID}}_{1}{\mathsf {)}}$
$\psi _{0}(\varphi ({\mathsf {<}}\Omega ,0,\Omega +1))$	${\mathsf {Aut(U(ID))}}$
$\psi _{0}(\Omega _{\omega })$	${\mathsf {ID}}_{<\omega }$	${\displaystyle {\mathsf {\Pi }}_{1}^{1}{\mathsf {-CA}}_{0}} ,$ Δ $\displaystyle {\ mathsf {\Delta }}_{2}^{1}{\mathsf {-CA}}_{0}}$		${\mathsf {MLW}}$
$\psi _{0}(\Omega _{\omega }\varepsilon _{0})$	${\mathsf {W-ID}}_{\omega }$	${\mathsf {\Pi }}_{1}^{1}{\mathsf {-CA}}$	${\mathsf {W-KPI}}$
$\psi _{0}(\Omega _{\omega +1})$	${\mathsf {ID}}_{\omega }$	${\mathsf {\Pi }}_{1}^{1}{\mathsf {-CA+BI}}$	${\mathsf {KPI}}$
$\psi _{\Omega }(\varepsilon _{K+1})$			${\mathsf {KP\Pi }}_{3}$
$\psi _{0}(\Omega _{\omega ^{\omega }})$	${\mathsf {ID}}_{<\omega ^{\omega }}$	${\mathsf {\Delta }}_{2}^{1}{\mathsf {-CR}}$
$\psi _{0}(\Omega _{\varepsilon _{0}})$	${\mathsf {ID}}_{<\varepsilon _{0}}$	${\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA}}$ , ${\mathsf {\Sigma }}_{2}^{1}{\mathsf {-AC}}$	${\mathsf {W-KPi}}$
$\psi _{0}(\Omega _{\Omega })$	${\mathsf {Aut(ID)}}$
$\psi (\varepsilon _{I+1})$		${\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA+BI}}$ , ${ \displaystyle {\mathsf {\Sigma }}_{2}^{1}{\mathsf {-AC+BI}}}$	${\mathsf {KPi}}$		${\mathsf {CZF+REA}}$	${\mathsf {T}}_{0}$
$\psi (\Omega _{I+\omega })$				${\mathsf {ML}}_{1}{\mathsf {W}}$
$\psi (\Omega _{L})$			${\mathsf {KPh}}$	${\mathsf {ML}}_{<\omega }{\mathsf {W}}$
$\psi (\Omega _{L^{*}})$				${\mathsf {Aut(MLW)}}$
$\psi _{\Omega }(\chi _{\varepsilon _{M+1}}(0))$		${\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA+BI+(M)}}$	${\mathsf {KPM}}$		${\mathsf {CZFM}}$
$\psi (\Omega _{M+\omega })$			${\mathsf {KPM}}^{+}$	${\mathsf {MLM}}$
$\Psi (\varepsilon _{K+1})$			${\mathsf {KP+\Pi }}_{3}-{\mathsf {Ref}}$
$\Psi _{(\omega ^{+};P_{0},\epsilon ,\epsilon ,0)}^{\varepsilon _ {\Xi +1}}$			${\mathsf {KP+\Pi }}_{\omega }-{\mathsf {Ref}}$
$\Psi _{(\omega ^{+};P_{0},\epsilon ,\epsilon ,0)}^{\varepsilon _ {\Upsilon +1}}$			${\mathsf {Stabilitet}}$
$\psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {I} +1})$		$\Sigma _{3}^{1}{\mathsf {-DC+BI}}$	${\mathsf {KP+\Pi }}_{1}{\mathsf {-samling}}$

Nyckel

Detta är en lista över symboler som används i den här tabellen:

• ψ representerar Buchholz psi om inte annat anges.
• Ψ representerar antingen Rathjens eller Stegerts Psi.
• φ representerar Veblens funktion.
• ω representerar den första transfinita ordinalen.
• ε _α representerar epsilontalen .
• ₀ Γ _α representerar gammatalen (Γ är Feferman–Schütte-ordinalen )
• Ω _α representerar de oräkneliga ordinalerna (Ω ₁ , förkortat Ω, är ω ₁ ).

Detta är en lista över de förkortningar som används i den här tabellen:

• Första ordningens aritmetik
  • ${\mathsf {Q}}$ är Robinson-arithmetik
  • ${\mathsf {PA}}^{-}$ är första ordningens teori för den icke-negativa delen av en diskret ordnad ring.
  • ${\mathsf {RFA}}$ är rudimentär funktionsaritmetik.
  • ₀${\mathsf {I\Delta }}_{0}$ är aritmetik med induktion begränsad till Δ -predikat utan något axiom som hävdar att exponentieringen är total.
  • ${\mathsf {EFA}}$ är elementär funktionsaritmetik .
  • ₀${\mathsf {I\Delta }}_{0}^{\mathsf {+}}$ är aritmetik med induktion begränsad till Δ -predikat utökade med ett axiom som hävdar att exponentieringen är total.
  • ${\mathsf {EFA}}^{\mathsf {n}}$ är elementär funktionsaritmetik förstärkt med ett axiom som säkerställer att varje element på den n -:e nivån ${\mathcal { E}}^{n}$ i Grzegorczyk-hierarkin är total.
  • ${\displaystyle {\mathsf {I\Delta }}_{0}^{\mathsf {n+}}} är$ I $\displaystyle {\mathsf {I\Delta }}_{0}^ {\mathsf {+}}}$ förstärkt med ett axiom som säkerställer att varje element i den n -:e nivån ${\mathcal {E}}^{n}$ i Grzegorczyk-hierarkin är total.
  • ${\mathsf {PRA}}$ är primitiv rekursiv aritmetik .
  • ${\mathsf {I\Sigma }}_{1}$ är aritmetik med induktion begränsad till Σ ₁ -predikat.
  • ${\mathsf {PA}}$ är Peano-arithmetik .
  • ${\mathsf {ID}}_{\nu }\#$ är ${\widehat {\mathsf {ID}}}_{\nu }$ men med induktion endast för positiva formler.
  • ${\widehat {\mathsf {ID}}}_{\nu }$ utökar PA med ν itererade fixpunkter av monotona operatorer.
  • ${\mathsf {U(PA)}}$ är inte precis ett första ordningens aritmetiskt system, utan fångar upp vad man kan få genom predikativt resonemang utifrån de naturliga talen.
  • ${\mathsf {Aut({\widehat {ID}})}}$ är en automorfism på ${\widehat {\mathsf {ID}}} _{\nu }$ .
  • ${\mathsf {ID}}_{\nu }$ utökar PA med ν itererade minst fixerade punkter av monotona operatorer.
  • ${\mathsf {U(ID}}_{\nu }{\mathsf {)}}$ är inte precis ett första ordningens aritmetiskt system, utan fångar vad man kan få genom predikativt resonemang baserat på ν gånger itererade generaliserade induktiva definitioner.
  • ${\mathsf {Aut(U(ID))}}$ är en automorfism på ${\mathsf {U(ID}}_ {\nu }{\mathsf {)}}$ .
  • ${\mathsf {W-ID}}_{\nu }$ är en försvagad version av ${\mathsf {ID}}_{\nu }$ baserad på W -typer.
• Andra ordningens aritmetik
  • ${\mathsf {RCA}}_{0}^{*}$ är en andra ordningens form av ${\displaystyle {\mathsf {EFA}}} som$ ibland används i omvänd matematik .
  • ${\mathsf {WKL}}_{0}^{*}$ är en andra ordningens form av ${\displaystyle {\mathsf {EFA}}} som$ ibland används i omvänd matematik.
  • ${\mathsf {RCA}}_{0}$ är rekursiv förståelse .
  • ${\mathsf {WKL}}_{0}$ är svagt Königs lemma .
  • ${\mathsf {ACA}}_{0}$ är aritmetisk förståelse .
  • ${\mathsf {ACA}}$ är ${\mathsf {ACA}}_{0}$ plus hela andra ordningens induktionsschema.
  • ${\mathsf {ATR}}_{0}$ är aritmetisk transfinit rekursion .
  • ${\mathsf {ATR}}$ är ${\mathsf {ATR}}_{0}$ plus hela andra ordningens induktionsschema.
  • ${\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA+BI+(M)}}$ är ${\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA+BI}}$ plus påståendet "every true ${\ mathsf {\Pi }}_{3}^{1}$ -mening med parametrar håller i en (räknebar kodad) $\beta$ -modell av ${\mathsf {\ Delta }}_{2}^{1}{\mathsf {-CA}}$ ".
• Kripke-Platek mängdlära
  • ${\mathsf {KP}}$ är Kripke-Platek mängdlära med oändlighetens axiom.
  • ${\mathsf {KP\omega }}$ är Kripke-Platek mängdteori, vars universum är en tillåten mängd som innehåller $\omega$ .
  • ${\mathsf {W-KPI}}$ är en försvagad version av ${\mathsf {KPI}}$ baserad på W-typer.
  • ${\mathsf {KPI}}$ hävdar att universum är en gräns för tillåtna mängder.
  • ${\mathsf {W-KPi}}$ är en försvagad version av ${\mathsf {KPi}}$ baserad på W-typer.
  • ${\mathsf {KPi}}$ hävdar att universum är otillgängliga set.
  • ${\mathsf {KPh}}$ hävdar att universum är hyperotillgängligt: ​​en otillgänglig mängd och en gräns för otillgängliga mängder.
  • ${\mathsf {KPM}}$ hävdar att universum är en Mahlo-uppsättning.
  • ${\displaystyle {\mathsf {KP+\Pi }}_{\mathsf {n}}-{\mathsf {Ref}}} är$ K $\displaystyle {\mathsf {KP} }}$ förstärkt med ett visst första ordningens reflektionsschema.
  • ${\mathsf {Stabilitet}}$ är KPi förstärkt med axiomet $\forall \alpha \ existerar \kappa \geq \alpha (L_{\kappa}\preceq _{1}L_{\kappa +\alpha })$ .
  • ${\mathsf {KPM}}^{+}$ är KPI förstärkt med påståendet "minst en rekursiv Mahlo-ordinal existerar".

En upphöjd nolla indikerar att $\in$ -induktion tas bort (gör teorin betydligt svagare).

• Typteori
  • ${\mathsf {CPRC}}$ är Herbelin-Patey-kalkylen för primitiva rekursiva konstruktioner.
  • ${\mathsf {ML}}_{\mathsf {n}}$ är typteori utan W-typer och med $n$ universum.
  • ${\mathsf {ML}}_{<\omega }$ är typteori utan W-typer och med ändligt många universum.
  • ${\mathsf {MLU}}$ är typteori med en nästa universumoperator.
  • ${\mathsf {MLS}}$ är typteori utan W-typer och med ett superuniversum.
  • ${\mathsf {Aut(ML)}}$ är en automorfism på typteori utan W-typer.
  • ${\mathsf {ML}}_{1}{\mathsf {V}}$ är typteori med ett universum och Aczels typ av iterativa mängder.
  • ${\mathsf {MLW}}$ är typteori med indexerade W-typer.
  • ${\mathsf {ML}}_{1}{\mathsf {W}}$ är typteori med W-typer och ett universum.
  • ${\mathsf {ML}}_{<\omega }{\mathsf {W}}$ är typteori med W-typer och ändligt många universum.
  • ${\mathsf {Aut(MLW)}}$ är en automorfism på typteori med W-typer.
  • ${\mathsf {MLM}}$ är typteori med ett Mahlo-universum.
• Konstruktiv mängdlära
  • ${\mathsf {CZF}}$ är Aczels konstruktiva mängdteori.
  • ${\mathsf {CZF+REA}}$ är ${\mathsf {CZF}}$ plus det vanliga förlängningsaxiomet.
  • ${\mathsf {CZF+REA+FZ}}_{2}$ är ${\mathsf {CZF+REA}}$ plus induktionsschemat för hela andra ordningen.
  • ${\mathsf {CZFM}}$ är ${\mathsf {CZF}}$ med ett Mahlo-universum.
• Explicit matematik
  • ${\mathsf {EM}}_{0}$ är grundläggande explicit matematik plus elementär förståelse
  • ${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+JR}}} är$ E $\displaystyle {\mathsf {EM}}_{0}}$ plus kopplingsregel
  • ${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+J}}} är$ E $\displaystyle {\mathsf {EM}}_{0}}$ plus sammanfogningsaxiom
  • $\displaystyle {\mathsf {EON}}}$${\mathsf {T}}_{0}$ är en svag variant av Fefermans T .
  • ${\mathsf {T}}_{0}$ är ${\mathsf {EM}}_{0}{\mathsf {+J+IG}}$ , där ${\mathsf {IG}}$ är induktiv generering.
  • ${\mathsf {T}}$ är ${\mathsf {EM}}_{0}{\mathsf {+J+IG+FZ}} _{2}$ , där ${\mathsf {FZ}}_{2}$ är hela andra ordningens induktionsschema.

Se även

• Ekvikonsistens
• Stor kardinalegendom
• Feferman–Schütte ordinal
• Bachmann–Howard ordinal
• Komplexitetsklass
• Gentzens konsistensbevis

Anteckningar

1. ^ För $1<n\leq \omega$

2. ^ Veblen-funktionen $\varphi$ med räkningsbart oändligt itererade minsta fixpunkter.

3. ^ Kan också vanligen skrivas som $\psi (\varepsilon _{\Omega +1})$ i Madores ψ.

4. ^ Använder Madores ψ snarare än Buchholzs ψ.

5. ^ Kan också vanligen skrivas som $\psi (\varepsilon _{\Omega _{\omega }+1})$ i Madores ψ.

6. ^ $K$ representerar den första rekursivt svagt kompakta ordinalen. Använder Arai's ψ snarare än Buchholz's ψ.

7. ^ Även den bevisteoretiska ordinalen för ${\displaystyle {\mathsf {Aut(W-ID)}}} ,$ eftersom mängden försvagning som ges av W-typerna inte är tillräcklig .

8. ^ $I$ representerar den första otillgängliga kardinalen. Använder Jägers ψ snarare än Buchholzs ψ.

9. ^ $L$ representerar gränsen för de $\omega$ -otillgängliga kardinalerna. Använder (förmodligen) Jägers ψ.

10. ^ $L^{*}$ representerar gränsen för de $\Omega$ -otillgängliga kardinalerna. Använder (förmodligen) Jägers ψ.

11. ^ $M$ representerar den första Mahlo-kardinalen. Använder Rathjens ψ snarare än Buchholzs ψ.

12. ^ $K$ representerar den första svagt kompakta kardinalen. Använder Rathjens Ψ snarare än Buchholzs ψ.

13. ^ $\Xi$ representerar den första $\Pi _{0}^{2}$ -obeskrivbara kardinal. Använder Stegerts Ψ snarare än Buchholzs ψ.

14. ^ $Y$ är den minsta $\alpha$ så att $\forall \theta <Y\exists \kappa <Y($ ' ${ \displaystyle \kappa }$ är $\theta$ -obeskrivbar') och ${\displaystyle \forall \theta <Y\forall \kappa <Y(} '$ κ $\displaystyle \ kappa }$ är $\theta$ -obeskrivbar $\rightarrow \theta <\kappa$ '). Använder Stegerts Ψ snarare än Buchholz's ψ.

15. ^ $M$ representerar den första Mahlo kardinal Använder (förmodligen) Rathjens ψ.

Citat

•   Buchholz, W.; Feferman, S.; Pohlers, W.; Sieg, W. (1981), Itererade induktiva definitioner och delsystem för analys , Lecture Notes in Math., vol. 897, Berlin: Springer-Verlag, doi : 10.1007/BFb0091894 , ISBN 978-3-540-11170-2
•    Pohlers, Wolfram (1989), Proof theory , Lecture Notes in Mathematics, vol. 1407, Berlin: Springer-Verlag, doi : 10.1007/978-3-540-46825-7 , ISBN 3-540-51842-8 , MR 1026933
•    Pohlers, Wolfram (1998), "Mängdteori och andra ordningens talteori", Handbook of Proof Theory , Studies in Logic and the Foundations of Mathematics, vol. 137, Amsterdam: Elsevier Science BV, s. 210–335, doi : 10.1016/S0049-237X(98)80019-0 , ISBN 0-444-89840-9 , MR 1640328
•    Rathjen, Michael (1990), "Ordinala notationer baserade på en svag Mahlo-kardinal." Arch . Matematik. Logic , 29 (4): 249–263, doi : 10.1007/BF01651328 , MR 1062729 , S2CID 14125063
•   Rathjen, Michael (2006), "The art of ordinal analysis" (PDF) , International Congress of Mathematicians , vol. II, Zürich: Eur. Matematik. Soc., s. 45–69, MR 2275588 , arkiverad från originalet 2009-12-22 {{ citation }} : CS1 underhåll: bot: ursprunglig URL-status okänd ( länk )
• Rose, HE (1984), Subrekursion. Functions and Hierarchies , Oxford logic guides, vol. 9, Oxford, New York: Clarendon Press, Oxford University Press
•    Schütte, Kurt (1977), Proof theory , Grundlehren der Mathematischen Wissenschaften, vol. 225, Berlin-New York: Springer-Verlag, s. xii+299, ISBN 3-540-07911-4 , MR 0505313
• Setzer, Anton (2004), "Proof theory of Martin-Löf type theory. An Overview" , Mathématiques et Sciences Humaines. Matematik och samhällsvetenskap (165): 59–99
•    Takeuti, Gaisi (1987), Proof theory , Studies in Logic and the Foundations of Mathematics, vol. 81 (andra upplagan), Amsterdam: North-Holland Publishing Co., ISBN 0-444-87943-9 , MR 0882549