Movatterモバイル変換


[0]ホーム

URL:


Jump to content
WikipediaThe Free Encyclopedia
Search

Ordinal analysis

From Wikipedia, the free encyclopedia
Mathematical technique used in proof theory
This article includes a list ofgeneral references, butit lacks sufficient correspondinginline citations. Please help toimprove this article byintroducing more precise citations.(September 2021) (Learn how and when to remove this message)

Inproof theory,ordinal analysis assignsordinals (oftenlarge countable ordinals) to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are oftenequiconsistent, and if one theory has a larger proof-theoretic ordinal than another it can often prove the consistency of the second theory.

In addition to obtaining the proof-theoretic ordinal of a theory, in practice ordinal analysis usually also yields various other pieces of information about the theory being analyzed, for example characterizations of the classes of provably recursive,hyperarithmetical, orΔ21{\displaystyle \Delta _{2}^{1}} functions of the theory.[1]

History

[edit]

The field of ordinal analysis was formed whenGerhard Gentzen in 1934 usedcut elimination to prove, in modern terms, that theproof-theoretic ordinal ofPeano arithmetic isε0. SeeGentzen's consistency proof.

Definition

[edit]

Ordinal analysis concerns true, effective (recursive) theories that can interpret a sufficient portion of arithmetic to make statements aboutordinal notations.

Theproof-theoretic ordinal of such a theoryT{\displaystyle T} is the supremum of theorder types of allordinal notations (necessarilyrecursive, see next section) that the theory can prove arewell founded—the supremum of all ordinalsα{\displaystyle \alpha } for which there exists anotationo{\displaystyle o} in Kleene's sense such thatT{\displaystyle T} proves thato{\displaystyle o} is an ordinal notation. Equivalently, it is the supremum of all ordinalsα{\displaystyle \alpha } such that there exists arecursive relationR{\displaystyle R} onω{\displaystyle \omega } (the set of natural numbers) thatwell-orders it with ordinalα{\displaystyle \alpha } and such thatT{\displaystyle T} provestransfinite induction of arithmetical statements forR{\displaystyle R}.

Ordinal notations

[edit]

Some theories, such as subsystems ofsecond-order arithmetic (Z2), have no conceptualization or way to make arguments about transfinite ordinals. For example, to formalize what it means for a subsystemT{\displaystyle T} of Z2 to "proveα{\displaystyle \alpha } well-ordered", we instead construct anordinal notation(A,<~){\displaystyle (A,{\tilde {<}})} with order typeα{\displaystyle \alpha }.T{\displaystyle T} can now work with various transfinite induction principles along(A,<~){\displaystyle (A,{\tilde {<}})}, which substitute for reasoning about set-theoretic ordinals.

However, some pathological notation systems exist that are unexpectedly difficult to work with. For example, Rathjen gives aprimitive recursive notation system(N,<T){\displaystyle (\mathbb {N} ,<_{T})} that is well-founded if and only if PA is consistent,[2]p. 3 despite having order typeω{\displaystyle \omega }. Including such a notation in the ordinal analysis of PA would result in the false equalityPTO(PA)=ω{\displaystyle {\mathsf {PTO(PA)}}=\omega }.

Upper bound

[edit]

Since an ordinal notation must be recursive, the proof-theoretic ordinal of any theory is less than or equal to theChurch–Kleene ordinalω1CK{\displaystyle \omega _{1}^{\mathrm {CK} }}. In particular, the proof-theoretic ordinal of aninconsistent theory is equal toω1CK{\displaystyle \omega _{1}^{\mathrm {CK} }}, because an inconsistent theory trivially proves that all ordinal notations are well-founded.

For any theory that's bothΣ11{\displaystyle \Sigma _{1}^{1}}-axiomatizable andΠ11{\displaystyle \Pi _{1}^{1}}-sound, the existence of a recursive ordering that the theory fails to prove is well-ordered follows from theΣ11{\displaystyle \Sigma _{1}^{1}} bounding theorem, and said provably well-founded ordinal notations are in fact well-founded byΠ11{\displaystyle \Pi _{1}^{1}}-soundness. Thus the proof-theoretic ordinal of aΠ11{\displaystyle \Pi _{1}^{1}}-sound theory that has aΣ11{\displaystyle \Sigma _{1}^{1}} axiomatization will always be a (countable)recursive ordinal, that is, strictly less thanω1CK{\displaystyle \omega _{1}^{\mathrm {CK} }}.[2]Theorem 2.21

Examples

[edit]

Theories with proof-theoretic ordinal ω

[edit]

Theories with proof-theoretic ordinal ω2

[edit]
  • RFA,rudimentary function arithmetic.[3]
  • 0, arithmetic with induction on Δ0-predicates without any axiom asserting that exponentiation is total.

Theories with proof-theoretic ordinal ω3

[edit]

Friedman'sgrand conjecture suggests that much "ordinary" mathematics can be proved in weak systems having this as their proof-theoretic ordinal.

Theories with proof-theoretic ordinal ωn (forn = 2, 3, ... ω)

[edit]

Theories with proof-theoretic ordinal ωω

[edit]

Theories with proof-theoretic ordinal ε0

[edit]

Theories with proof-theoretic ordinal theFeferman–Schütte ordinal Γ0

[edit]

This ordinal is sometimes considered to be the upper limit for "predicative" theories.

Theories with proof-theoretic ordinal theBachmann–Howard ordinal

[edit]

The Kripke–Platek or CZF set theories are weak set theories without axioms for the full powerset given as set of all subsets. Instead, they tend to either have axioms of restricted separation and formation of new sets, or they grant existence of certain function spaces (exponentiation) instead of carving them out from bigger relations.

Theories with larger proof-theoretic ordinals

[edit]
Unsolved problem in mathematics
What is the proof-theoretic ordinal of full second-order arithmetic?[4]
More unsolved problems in mathematics

Most theories capable of describing the power set of the natural numbers have proof-theoretic ordinals that are so large that no explicit combinatorial description has yet been given. This includesΠ21CA0{\displaystyle \Pi _{2}^{1}-CA_{0}}, fullsecond-order arithmetic (Π1CA0{\displaystyle \Pi _{\infty }^{1}-CA_{0}}) and set theories with powersets includingZF and ZFC.[7] The strength ofintuitionistic ZF (IZF) equals that of ZF.

Table of ordinal analyses

[edit]
Table of proof-theoretic ordinals
OrdinalFirst-order arithmeticSecond-order arithmeticKripke–Platek set theoryType theoryConstructive set theoryExplicit mathematics
ω{\displaystyle \omega }Q{\displaystyle {\mathsf {Q}}},PA{\displaystyle {\mathsf {PA}}^{-}}
ω2{\displaystyle \omega ^{2}}RFA{\displaystyle {\mathsf {RFA}}},IΔ0{\displaystyle {\mathsf {I\Delta }}_{0}}
ω3{\displaystyle \omega ^{3}}EFA{\displaystyle {\mathsf {EFA}}},IΔ0+{\displaystyle {\mathsf {I\Delta }}_{0}^{\mathsf {+}}},BΣ1{\displaystyle {\mathsf {B}}\Sigma _{1}}[8]Theorem 4.1RCA0{\displaystyle {\mathsf {RCA}}_{0}^{*}},WKL0{\displaystyle {\mathsf {WKL}}_{0}^{*}}
ωn{\displaystyle \omega ^{n}}[1]EFAn{\displaystyle {\mathsf {EFA}}^{\mathsf {n}}},IΔ0n+{\displaystyle {\mathsf {I\Delta }}_{0}^{\mathsf {n+}}}
ωω{\displaystyle \omega ^{\omega }}PRA{\displaystyle {\mathsf {PRA}}},IΣ1{\displaystyle {\mathsf {I\Sigma }}_{1}}[9]p. 13RCA0{\displaystyle {\mathsf {RCA}}_{0}}[9]p. 13,WKL0{\displaystyle {\mathsf {WKL}}_{0}}[9]p. 13CPRC{\displaystyle {\mathsf {CPRC}}}
ωωωω{\displaystyle \omega ^{\omega ^{\omega ^{\omega }}}}IΣ3{\displaystyle {\mathsf {I}}\Sigma _{3}}[10][9]p. 13RCA0+(Π20)IND{\displaystyle {\mathsf {RCA}}_{0}+(\Pi _{2}^{0})^{-}{\mathsf {-IND}}}[11]: 40 
ε0{\displaystyle \varepsilon _{0}}PA{\displaystyle {\mathsf {PA}}}[9]p. 13ACA0{\displaystyle {\mathsf {ACA}}_{0}}[9]p. 13,Σ11AC0{\displaystyle {\mathsf {\Sigma }}_{1}^{1}{\mathsf {-AC}}_{0}}[9]p. 13,R-EΩ^{\displaystyle {\text{R-}}{\widehat {\mathbf {E} {\boldsymbol {\Omega }}}}}[12]p. 8,RCA{\displaystyle {\mathsf {RCA}}}[13]p. 148,WKL{\displaystyle {\mathsf {WKL}}}[13]p. 148,Δ11CA0{\displaystyle {\mathsf {\Delta }}_{1}^{1}{\mathsf {-CA}}_{0}}[14]KPur{\displaystyle \mathrm {KPu} ^{r}}[15]p. 869EM0{\displaystyle {\mathsf {EM}}_{0}}
εω{\displaystyle \varepsilon _{\omega }}ACA0+iRT{\displaystyle {\mathsf {ACA}}_{0}+{\mathsf {iRT}}},[16]RCA0+YnX(TJ(n,X,Y)){\displaystyle {\mathsf {RCA}}_{0}+\forall Y\forall n\exists X({\textrm {TJ}}(n,X,Y))}[17]: 8 
εε0{\displaystyle \varepsilon _{\varepsilon _{0}}}ACA{\displaystyle {\mathsf {ACA}}}[18]p. 959
ζ0{\displaystyle \zeta _{0}}ACA0+XY(TJ(ω,X,Y)){\displaystyle {\mathsf {ACA}}_{0}+\forall X\exists Y({\textrm {TJ}}(\omega ,X,Y))},[19][17]p1(ACA0){\displaystyle {\mathsf {p}}_{1}({\mathsf {ACA}}_{0})},[20]: 7 RFN0{\displaystyle {\mathsf {RFN}}_{0}}[19]p. 17,ACA0+(BR){\displaystyle {\mathsf {ACA}}_{0}+({\mathsf {BR}})}[19]p. 5
φ(2,ε0){\displaystyle \varphi (2,\varepsilon _{0})}RFN{\displaystyle {\mathsf {RFN}}},ACA+XY(TJ(ω,X,Y)){\displaystyle {\mathsf {ACA}}+\forall X\exists Y({\textrm {TJ}}(\omega ,X,Y))}[19]p. 52
φ(ω,0){\displaystyle \varphi (\omega ,0)}ID1#{\displaystyle {\mathsf {ID}}_{1}\#},TID0{\displaystyle {\mathsf {TID}}_{0}}[21]p. 137Δ11CR{\displaystyle {\mathsf {\Delta }}_{1}^{1}{\mathsf {-CR}}},Σ11DC0{\displaystyle \Sigma _{1}^{1}{\mathsf {-DC}}_{0}}[22]EM0+JR{\displaystyle {\mathsf {EM}}_{0}{\mathsf {+JR}}}
φ(ε0,0){\displaystyle \varphi (\varepsilon _{0},0)}ID^1{\displaystyle {\widehat {\mathsf {ID}}}_{1}},KFL{\displaystyle {\mathsf {KFL}}}[23]p. 17,KF{\displaystyle {\mathsf {KF}}}[23]p. 17Δ11CA{\displaystyle {\mathsf {\Delta }}_{1}^{1}{\mathsf {-CA}}}[24]p. 140,Σ11AC{\displaystyle {\mathsf {\Sigma }}_{1}^{1}{\mathsf {-AC}}}[24]p. 140,Σ11DC{\displaystyle {\mathsf {\Sigma }}_{1}^{1}{\mathsf {-DC}}}[24]p. 140,W-EΩ^{\displaystyle {\text{W-}}{\widehat {\mathbf {E} {\boldsymbol {\Omega }}}}}[12]p. 8KPur+(INDN){\displaystyle \mathrm {KPu} ^{r}+(\mathrm {IND} _{N})}[15]p. 870ML1{\displaystyle {\mathsf {ML}}_{1}}EM0+J{\displaystyle {\mathsf {EM}}_{0}{\mathsf {+J}}}
φ(εε0,0){\displaystyle \varphi (\varepsilon _{\varepsilon _{0}},0)}EΩ^{\displaystyle {\widehat {\mathbf {E} {\boldsymbol {\Omega }}}}}[12]p. 27,EID^1{\displaystyle {\widehat {\mathbf {EID} }}_{\boldsymbol {1}}}[12]p. 27
φ(φ(ω,0),0){\displaystyle \varphi (\varphi (\omega ,0),0)}PRSω{\displaystyle \mathrm {PRS} \omega }[25]p. 9
φ(<Ω,0){\displaystyle \varphi ({\mathsf {<}}\Omega ,0)}[2]Aut(ID#){\displaystyle {\mathsf {Aut(ID\#)}}}
Γ0{\displaystyle \Gamma _{0}}ID^<ω{\displaystyle {\widehat {\mathsf {ID}}}_{<\omega }},[26]U(PA){\displaystyle {\mathsf {U(PA)}}},KFL{\displaystyle \mathbf {KFL} ^{*}}[23]p. 22,KF{\displaystyle \mathbf {KF} ^{*}}[23]p. 22,U(NFA){\displaystyle {\mathcal {U}}(\mathrm {NFA} )},[27]TID0+{\displaystyle {\mathsf {TID}}_{0}^{+}}[21]p. 137ATR0{\displaystyle {\mathsf {ATR}}_{0}},Δ11CA+BR{\displaystyle {\mathsf {\Delta }}_{1}^{1}{\mathsf {-CA+BR}}},Δ11CA0+(SUB){\displaystyle \Delta _{1}^{1}\mathrm {-CA} _{0}+\mathrm {(SUB)} },[28]FP0{\displaystyle \mathrm {FP} _{0}}[29]p. 26KPi0{\displaystyle {\mathsf {KPi}}^{0}}[15]p. 878,KPu0+(BR){\displaystyle {\mathsf {KPu}}^{0}+(\mathrm {BR} )}[15]p. 878ML<ω{\displaystyle {\mathsf {ML}}_{<\omega }},MLU{\displaystyle {\mathsf {MLU}}}
Γωω{\displaystyle \Gamma _{\omega ^{\omega }}}KPI0+(Σ1Iω){\displaystyle {\mathsf {KPI}}^{0}+({\mathsf {\Sigma _{1}-I}}_{\omega })}[30]p. 13
Γε0{\displaystyle \Gamma _{\varepsilon _{0}}}ID^ω{\displaystyle {\widehat {\mathsf {ID}}}_{\omega }}ATR{\displaystyle {\mathsf {ATR}}}[31]KPI0+FIω{\displaystyle {\mathsf {KPI}}^{0}{\mathsf {+F-I}}_{\omega }}
φ(1,ω,0){\displaystyle \varphi (1,\omega ,0)}ID^<ωω{\displaystyle {\widehat {\mathsf {ID}}}_{<\omega ^{\omega }}}ATR0+(Σ11DC){\displaystyle {\mathsf {ATR}}_{0}+({\mathsf {\Sigma }}_{1}^{1}{\mathsf {-DC}})}[20]: 7 KPi0+Σ1Iω{\displaystyle {\mathsf {KPi}}^{0}{\mathsf {+\Sigma _{1}-I}}_{\omega }}
φ(1,ε0,0){\displaystyle \varphi (1,\varepsilon _{0},0)}ID^<ε0{\displaystyle {\widehat {\mathsf {ID}}}_{<\varepsilon _{0}}}ATR+(Σ11DC){\displaystyle {\mathsf {ATR}}+({\mathsf {\Sigma }}_{1}^{1}{\mathsf {-DC}})}[20]: 7 KPi0+FIω{\displaystyle {\mathsf {KPi}}^{0}{\mathsf {+F-I}}_{\omega }}
φ(1,Γ0,0){\displaystyle \varphi (1,\Gamma _{0},0)}ID^<Γ0{\displaystyle {\widehat {\mathsf {ID}}}_{<\Gamma _{0}}}MLS{\displaystyle {\mathsf {MLS}}}
φ(2,0,0){\displaystyle \varphi (2,0,0)}Aut(ID^){\displaystyle {\mathsf {Aut({\widehat {ID}})}}},FTR0{\displaystyle {\mathsf {FTR}}_{0}}[32]AxΣ11ACTR0{\displaystyle Ax_{\Sigma _{1}^{1}{\mathsf {-AC}}}{\mathsf {TR}}_{0}}[33]p. 1167,AxATR+Σ11DCRFN0{\displaystyle Ax_{{\mathsf {ATR}}+\Sigma _{1}^{1}{\mathsf {-DC}}}{\mathsf {RFN}}_{0}}[33]p. 1167KPh0{\displaystyle {\mathsf {KPh}}^{0}}Aut(ML){\displaystyle {\mathsf {Aut(ML)}}}
φ(2,0,ε0){\displaystyle \varphi (2,0,\varepsilon _{0})}FTR{\displaystyle {\mathsf {FTR}}}[32]AxΣ11ACTR{\displaystyle Ax_{\Sigma _{1}^{1}{\mathsf {-AC}}}{\mathsf {TR}}}[33]p. 1167,AxATR+Σ11DCRFN{\displaystyle Ax_{{\mathsf {ATR}}+\Sigma _{1}^{1}{\mathsf {-DC}}}{\mathsf {RFN}}}[33]p. 1167
φ(2,ε0,0){\displaystyle \varphi (2,\varepsilon _{0},0)}KPh0+(FIω){\displaystyle {\mathsf {KPh}}_{0}+({\mathsf {F-I}}_{\omega })}[32]: 11 
φ(ω,0,0){\displaystyle \varphi (\omega ,0,0)}(Π21RFN)0Σ11DC{\displaystyle (\Pi _{2}^{1}{\mathsf {-RFN}})_{0}^{\Sigma _{1}^{1}{\mathsf {-DC}}}}[34]p. 233,Σ11TDC0{\displaystyle \Sigma _{1}^{1}{\mathsf {-TDC}}_{0}}[34]p. 233KPm0{\displaystyle {\mathsf {KPm}}^{0}}[35]p. 276EMA{\displaystyle {\mathsf {EMA}}}[35]p. 276
φ(ε0,0,0){\displaystyle \varphi (\varepsilon _{0},0,0)}(Π21RFN)Σ11DC{\displaystyle (\Pi _{2}^{1}{\mathsf {-RFN}})^{\Sigma _{1}^{1}{\mathsf {-DC}}}}[34]p. 233,Σ11TDC{\displaystyle \Sigma _{1}^{1}{\mathsf {-TDC}}}[20]KPm0+(LIN){\displaystyle {\mathsf {KPm}}^{0}+({\mathcal {L}}^{*}{\mathsf {-I}}_{\mathsf {N}})}[35]p. 277EMA+(LIN){\displaystyle {\mathsf {EMA}}+(\mathbb {L} {\mathsf {-I}}_{\mathsf {N}})}[35]p. 277
φ(1,0,0,0){\displaystyle \varphi (1,0,0,0)}p1(Σ11TDC0){\displaystyle {\mathsf {p}}_{1}(\Sigma _{1}^{1}{\mathsf {-TDC}}_{0})}[20]: 7 
ψΩ1(ΩΩω){\displaystyle \psi _{\Omega _{1}}(\Omega ^{\Omega ^{\omega }})}RCA0+Π11CA{\displaystyle {\mathsf {RCA}}_{0}^{*}+\Pi _{1}^{1}{\mathsf {-CA}}^{-}},[36]p3(ACA0){\displaystyle {\mathsf {p}}_{3}({\mathsf {ACA}}_{0})}[20]: 7 
ϑ(ΩΩ){\displaystyle \vartheta (\Omega ^{\Omega })}TID{\displaystyle {\mathsf {TID}}},TID1{\displaystyle {\mathsf {TID}}_{1}}[21]p. 171p1(p3(ACA0)){\displaystyle {\mathsf {p}}_{1}({\mathsf {p}}_{3}({\mathsf {ACA}}_{0}))}[20]: 7 FIT{\displaystyle {\mathsf {FIT}}}[21]p. 171
ψ0(εΩ+1){\displaystyle \psi _{0}(\varepsilon _{\Omega +1})}[3]ID1{\displaystyle {\mathsf {ID}}_{1}}W-EΩ~{\displaystyle {\text{W-}}{\widetilde {\mathbf {E} {\boldsymbol {\Omega }}}}}[12]p. 8KP{\displaystyle {\mathsf {KP}}},[2]KPω{\displaystyle {\mathsf {KP\omega }}},KPu{\displaystyle \mathrm {KPu} }[15]p. 869ML1V{\displaystyle {\mathsf {ML}}_{1}{\mathsf {V}}}CZF{\displaystyle {\mathsf {CZF}}}EON{\displaystyle {\mathsf {EON}}}
ψ(εΩ+ε0){\displaystyle \psi (\varepsilon _{\Omega +\varepsilon _{0}})}EΩ~{\displaystyle {\widetilde {\mathbf {E} {\boldsymbol {\Omega }}}}}[12]p. 31,EID~1{\displaystyle {\widetilde {\mathbf {EID} }}_{\boldsymbol {1}}}[12]p. 31,ACA+(Π11-CA){\displaystyle \mathbf {ACA} +(\Pi _{1}^{1}{\text{-CA}})^{-}}[12]p. 31
ψ(εΩ+Ω){\displaystyle \psi (\varepsilon _{\Omega +\Omega })}(ID12)0+BR{\displaystyle ({\mathsf {ID}}_{1}^{2})_{0}+{\mathsf {BR}}}[37]
ψ(εεΩ+1){\displaystyle \psi (\varepsilon _{\varepsilon _{\Omega +1}})}EΩ{\displaystyle \mathbf {E} {\boldsymbol {\Omega }}}[12]p. 33,EID1{\displaystyle \mathbf {EID} _{\boldsymbol {1}}}[12]p. 33,ACA+(Π11-CA)+(BIPR){\displaystyle \mathbf {ACA} +(\Pi _{1}^{1}{\text{-CA}})^{-}+(\mathrm {BI} _{\mathrm {PR} })^{-}}[12]p. 33
ψ0(ΓΩ+1){\displaystyle \psi _{0}(\Gamma _{\Omega +1})}[4]U(ID1){\displaystyle {\mathsf {U(ID}}_{1}{\mathsf {)}}},ID^<ω{\displaystyle {\widehat {\mathsf {ID}}}_{<\omega }^{\bullet }}[29]p. 26,Σ11DC0+(SUB){\displaystyle \Sigma _{1}^{1}{\mathsf {-DC}}_{0}^{\bullet }+({\mathsf {SUB}}^{\bullet })}[29]p. 26,ATR0{\displaystyle {\mathsf {ATR}}_{0}^{\bullet }}[29]p. 26,Σ11AC0+(SUB){\displaystyle \Sigma _{1}^{1}{\mathsf {-AC}}_{0}^{\bullet }+({\mathsf {SUB}}^{\bullet })}[29]p. 26,U(ID1){\displaystyle {\mathcal {U}}({\mathsf {ID}}_{1})}[29]p. 26FP0{\displaystyle {\mathsf {FP}}_{0}^{\bullet }}[29]p. 26,ATR0{\displaystyle {\mathsf {ATR}}_{0}^{\bullet }}[29]p. 26
ψ0(φ(<Ω,0,Ω+1)){\displaystyle \psi _{0}(\varphi ({\mathsf {<}}\Omega ,0,\Omega +1))}Aut(U(ID)){\displaystyle {\mathsf {Aut(U(ID))}}}
ψ0(Ωω){\displaystyle \psi _{0}(\Omega _{\omega })}ID<ω{\displaystyle {\mathsf {ID}}_{<\omega }}[4]p. 28Π11CA0{\displaystyle {\mathsf {\Pi }}_{1}^{1}{\mathsf {-CA}}_{0}}[4]p. 28,Δ21CA0{\displaystyle {\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA}}_{0}}MLW{\displaystyle {\mathsf {MLW}}}SUS+(SIN){\displaystyle {\mathsf {SUS}}+({\mathsf {S}}-{\mathsf {I}}_{\mathsf {N}})}[38]p. 27
ψ0(Ωωωω){\displaystyle \psi _{0}(\Omega _{\omega }\omega ^{\omega })}Π11CA0+Π21IND{\displaystyle \Pi _{1}^{1}{\mathsf {-CA}}_{0}+\Pi _{2}^{1}{\mathsf {-IND}}}[39]
ψ0(Ωωε0){\displaystyle \psi _{0}(\Omega _{\omega }\varepsilon _{0})}WIDω{\displaystyle {\mathsf {W-ID}}_{\omega }}Π11CA{\displaystyle {\mathsf {\Pi }}_{1}^{1}{\mathsf {-CA}}}[40]p. 14WKPI{\displaystyle {\mathsf {W-KPI}}}
ψ0(ΩωΩ){\displaystyle \psi _{0}(\Omega _{\omega }\Omega )}Π11CA+BR{\displaystyle \Pi _{1}^{1}{\mathsf {-CA+BR}}}[41]
ψ0(Ωωω){\displaystyle \psi _{0}(\Omega _{\omega }^{\omega })}Π11CA0+Π21BI{\displaystyle \Pi _{1}^{1}{\mathsf {-CA}}_{0}+\Pi _{2}^{1}{\mathsf {-BI}}}[39]
ψ0(Ωωωω){\displaystyle \psi _{0}(\Omega _{\omega }^{\omega ^{\omega }})}Π11CA0+Π21BI+Π31IND{\displaystyle \Pi _{1}^{1}{\mathsf {-CA}}_{0}+\Pi _{2}^{1}{\mathsf {-BI}}+\Pi _{3}^{1}{\mathsf {-IND}}}[39]
ψ0(εΩω+1){\displaystyle \psi _{0}(\varepsilon _{\Omega _{\omega }+1})}[5]IDω{\displaystyle {\mathsf {ID}}_{\omega }}Π11CA+BI{\displaystyle {\mathsf {\Pi }}_{1}^{1}{\mathsf {-CA+BI}}}KPI{\displaystyle {\mathsf {KPI}}}
ψ0(Ωωω){\displaystyle \psi _{0}(\Omega _{\omega ^{\omega }})}ID<ωω{\displaystyle {\mathsf {ID}}_{<\omega ^{\omega }}}Δ21CR{\displaystyle {\mathsf {\Delta }}_{2}^{1}{\mathsf {-CR}}}[4]p. 28SUS+(NIN){\displaystyle {\mathsf {SUS}}+({\mathsf {N}}-{\mathsf {I}}_{\mathsf {N}})}[38]p. 27
ψ0(Ωε0){\displaystyle \psi _{0}(\Omega _{\varepsilon _{0}})}ID<ε0{\displaystyle {\mathsf {ID}}_{<\varepsilon _{0}}}Δ21CA{\displaystyle {\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA}}}[4]p. 28,Σ21AC{\displaystyle {\mathsf {\Sigma }}_{2}^{1}{\mathsf {-AC}}}WKPi{\displaystyle {\mathsf {W-KPi}}}SUS+(LIN){\displaystyle {\mathsf {SUS}}+(\mathrm {L} -{\mathsf {I}}_{\mathsf {N}})}[38]p. 27
ψ0(ΩΩ){\displaystyle \psi _{0}(\Omega _{\Omega })}Aut(ID){\displaystyle {\mathsf {Aut(ID)}}}[6]
ψΩ1(εΩΩ+1){\displaystyle \psi _{\Omega _{1}}(\varepsilon _{\Omega _{\Omega }+1})}ID{\displaystyle {\mathsf {ID}}_{\prec ^{*}}},BID2{\displaystyle {\mathsf {BID}}^{2*}},ID2+BI{\displaystyle {\mathsf {ID}}^{2*}+{\mathsf {BI}}}[42]KPl{\displaystyle {\mathsf {KPl}}^{*}},KPlΩr{\displaystyle {\mathsf {KPl}}_{\Omega }^{r}}
ψ0(Φ1(0)){\displaystyle \psi _{0}(\Phi _{1}(0))}Π11TR0{\displaystyle \Pi _{1}^{1}{\mathsf {-TR}}_{0}},Π11TR0+Δ21CA0{\displaystyle \Pi _{1}^{1}{\mathsf {-TR}}_{0}+\Delta _{2}^{1}{\mathsf {-CA}}_{0}},Δ21CA+BI(implΣ21){\displaystyle \Delta _{2}^{1}{\mathsf {-CA+BI(impl-}}\Sigma _{2}^{1})},Δ21CA+BR(implΣ21){\displaystyle \Delta _{2}^{1}{\mathsf {-CA+BR(impl-}}\Sigma _{2}^{1})},AUTID0pos{\displaystyle \mathbf {AUT-ID} _{0}^{pos}},AUTID0mon{\displaystyle \mathbf {AUT-ID} _{0}^{mon}}[42]: 72 KPiw+FOUNDR(impl)Σ){\displaystyle {\mathsf {KPi}}^{w}+{\mathsf {FOUNDR}}({\mathsf {impl-}})\Sigma )},[42]: 72 KPiw+FOUND(impl)Σ){\displaystyle {\mathsf {KPi}}^{w}+{\mathsf {FOUND}}({\mathsf {impl-}})\Sigma )},[42]: 72 

AUTKPlr{\displaystyle \mathbf {AUT-KPl} ^{r}},AUTKPlr+KPir{\displaystyle \mathbf {AUT-KPl} ^{r}+\mathbf {KPi} ^{r}}[42]: 72 

ψ0(Φ1(0)ε0){\displaystyle \psi _{0}(\Phi _{1}(0)\varepsilon _{0})}Π11TR{\displaystyle \Pi _{1}^{1}{\mathsf {-TR}}},AUTIDpos{\displaystyle \mathbf {AUT-ID} ^{pos}},AUTIDmon{\displaystyle \mathbf {AUT-ID} ^{mon}}[42]: 72 AUTKPlw{\displaystyle \mathbf {AUT-KPl} ^{w}}[42]: 72 
ψ0(εΦ1(0)+1){\displaystyle \psi _{0}(\varepsilon _{\Phi _{1}(0)+1})}Π11TR+(BI){\displaystyle \Pi _{1}^{1}{\mathsf {-TR}}+({\mathsf {BI}})},AUTID2pos{\displaystyle \mathbf {AUT-ID} _{2}^{pos}},AUTID2mon{\displaystyle \mathbf {AUT-ID} _{2}^{mon}}[42]: 72 AUTKPl{\displaystyle \mathbf {AUT-KPl} }[42]: 72 
ψ0(Φ1(ε0)){\displaystyle \psi _{0}(\Phi _{1}(\varepsilon _{0}))}Π11TR+Δ21CA{\displaystyle \Pi _{1}^{1}{\mathsf {-TR}}+\Delta _{2}^{1}{\mathsf {-CA}}},Π11TR+Σ21AC{\displaystyle \Pi _{1}^{1}{\mathsf {-TR}}+\Sigma _{2}^{1}{\mathsf {-AC}}}[42]: 72 AUTKPlw+KPiw{\displaystyle \mathbf {AUT-KPl} ^{w}+\mathbf {KPi} ^{w}}[42]: 72 
ψ0(Φω(0)){\displaystyle \psi _{0}(\Phi _{\omega }(0))}Δ21TR0{\displaystyle \Delta _{2}^{1}{\mathsf {-TR}}_{0}},Σ21TRDC0{\displaystyle \Sigma _{2}^{1}{\mathsf {-TRDC}}_{0}},Δ21CA0+(Σ21BI){\displaystyle \Delta _{2}^{1}{\mathsf {-CA}}_{0}+(\Sigma _{2}^{1}{\mathsf {-BI}})}[42]: 72 KPir+(ΣFOUND){\displaystyle \mathbf {KPi} ^{r}+(\Sigma {\mathsf {-FOUND}})},KPir+(ΣREC){\displaystyle \mathbf {KPi} ^{r}+(\Sigma {\mathsf {-REC}})}[42]: 72 
ψ0(Φε0(0)){\displaystyle \psi _{0}(\Phi _{\varepsilon _{0}}(0))}Δ21TR{\displaystyle \Delta _{2}^{1}{\mathsf {-TR}}},Σ21TRDC{\displaystyle \Sigma _{2}^{1}{\mathsf {-TRDC}}},Δ21CA+(Σ21BI){\displaystyle \Delta _{2}^{1}{\mathsf {-CA}}+(\Sigma _{2}^{1}{\mathsf {-BI}})}[42]: 72 KPiw+(ΣFOUND){\displaystyle \mathbf {KPi} ^{w}+(\Sigma {\mathsf {-FOUND}})},KPiw+(ΣREC){\displaystyle \mathbf {KPi} ^{w}+(\Sigma {\mathsf {-REC}})}[42]: 72 
ψ(εI+1){\displaystyle \psi (\varepsilon _{I+1})}[7]Δ21CA+BI{\displaystyle {\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA+BI}}}[4]p. 28,Σ21AC+BI{\displaystyle {\mathsf {\Sigma }}_{2}^{1}{\mathsf {-AC+BI}}}KPi{\displaystyle {\mathsf {KPi}}}CZF+REA{\displaystyle {\mathsf {CZF+REA}}}T0{\displaystyle {\mathsf {T}}_{0}}
ψ(ΩI+ω){\displaystyle \psi (\Omega _{I+\omega })}ML1W{\displaystyle {\mathsf {ML}}_{1}{\mathsf {W}}}[43]: 38 
ψ(ΩL){\displaystyle \psi (\Omega _{L})}[8]KPh{\displaystyle {\mathsf {KPh}}}ML<ωW{\displaystyle {\mathsf {ML}}_{<\omega }{\mathsf {W}}}
ψ(ΩL){\displaystyle \psi (\Omega _{L^{*}})}[9]Aut(MLW){\displaystyle {\mathsf {Aut(MLW)}}}
ψΩ(χεM+1(0)){\displaystyle \psi _{\Omega }(\chi _{\varepsilon _{M+1}}(0))}[10]Δ21CA+BI+(M){\displaystyle {\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA+BI+(M)}}}[44]KPM{\displaystyle {\mathsf {KPM}}}CZFM{\displaystyle {\mathsf {CZFM}}}
ψ(ΩM+ω){\displaystyle \psi (\Omega _{M+\omega })}[11]KPM+{\displaystyle {\mathsf {KPM}}^{+}}[45]TTM{\displaystyle {\mathsf {TTM}}}[45]
ΨΩ0(εK+1){\displaystyle \Psi _{\Omega }^{0}(\varepsilon _{K+1})}[12]KP+Π3Ref{\displaystyle {\mathsf {KP+\Pi }}_{3}-{\mathsf {Ref}}}[46]
Ψ(ω+;P0,ϵ,ϵ,0)εΞ+1{\displaystyle \Psi _{(\omega ^{+};P_{0},\epsilon ,\epsilon ,0)}^{\varepsilon _{\Xi +1}}}[13]KP+ΠωRef{\displaystyle {\mathsf {KP+\Pi }}_{\omega }-{\mathsf {Ref}}}[47]
Ψ(ω+;P0,ϵ,ϵ,0)εΥ+1{\displaystyle \Psi _{(\omega ^{+};P_{0},\epsilon ,\epsilon ,0)}^{\varepsilon _{\Upsilon +1}}}[14]Stability{\displaystyle {\mathsf {Stability}}}[47]
ψω1CK(εS++1){\displaystyle \psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {S} ^{+}+1})}[48]KPω+Π11Ref{\displaystyle {\mathsf {KP}}\omega +\Pi _{1}^{1}-{\mathsf {Ref}}},[48]KPω+(MΣ1V){\displaystyle {\mathsf {KP}}\omega +(M\prec _{\Sigma _{1}}V)}[49]
ψω1CK(εI+1){\displaystyle \psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {I} +1})}[48]Σ31DC+BI{\displaystyle \Sigma _{3}^{1}{\mathsf {-DC+BI}}},Σ31AC+BI{\displaystyle \Sigma _{3}^{1}{\mathsf {-AC+BI}}}KPω+Π1Collection+(V=L){\displaystyle {\mathsf {KP}}\omega +\Pi _{1}-{\mathsf {Collection}}+(V=L)}
ψω1CK(εIN+1){\displaystyle \psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {I} _{N}+1})}[50]ΣN+21DC+BI{\displaystyle \Sigma _{N+2}^{1}{\mathsf {-DC+BI}}},ΣN+21AC+BI{\displaystyle \Sigma _{N+2}^{1}{\mathsf {-AC+BI}}}KPω+ΠNCollection+(V=L){\displaystyle {\mathsf {KP}}\omega +\Pi _{N}-{\mathsf {Collection}}+(V=L)}
ψω1CK(Iω){\displaystyle \psi _{\omega _{1}^{CK}}(\mathbb {I} _{\omega })}[50]PA+N<ωTI[Π01,ψω1CK(εIN+1)]{\displaystyle {\mathsf {PA}}+\bigcup \limits _{N<\omega }{\mathsf {TI}}[\Pi _{0}^{1-},\psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {I} _{N}+1})]}[50]Z2{\displaystyle \mathbf {Z} _{2}},Π1CA{\displaystyle \Pi _{\infty }^{1}-{\mathsf {CA}}}, BarKP+ΠωsetSeparation{\displaystyle {\mathsf {KP}}+\Pi _{\omega }^{\text{set}}-{\mathsf {Separation}}}λ2{\displaystyle \lambda 2}[51]CZF+Sep{\displaystyle {\mathsf {CZF+Sep}}}[52]

Key

[edit]

This is a list of symbols used in this table:

This is a list of the abbreviations used in this table:

In general, a subscript 0 means that the induction scheme is restricted to a single set induction axiom.

A superscript zero indicates that{\displaystyle \in }-induction is removed (making the theory significantly weaker).

See also

[edit]

Notes

[edit]
1.^ For1<nω{\displaystyle 1<n\leq {\mathsf {\omega }}}
2.^ The Veblen functionφ{\displaystyle \varphi } with countably infinitely iterated least fixed points.[clarification needed]
3.^ Can also be commonly written asψ(εΩ+1){\displaystyle \psi (\varepsilon _{\Omega +1})} in Madore's ψ.
4.^ Uses Madore's ψ rather than Buchholz's ψ.
5.^ Can also be commonly written asψ(εΩω+1){\displaystyle \psi (\varepsilon _{\Omega _{\omega }+1})} in Madore's ψ.
6.^K{\displaystyle K} represents the first recursively weakly compact ordinal. Uses Arai's ψ rather than Buchholz's ψ.
7.^ Also the proof-theoretic ordinal ofAut(WID){\displaystyle {\mathsf {Aut(W-ID)}}}, as the amount of weakening given by the W-types is not enough.
8.^I{\displaystyle I} represents the first inaccessible cardinal. Uses Jäger's ψ rather than Buchholz's ψ.
9.^L{\displaystyle L} represents the limit of theω{\displaystyle \omega }-inaccessible cardinals. Uses (presumably) Jäger's ψ.
10.^L{\displaystyle L^{*}}represents the limit of theΩ{\displaystyle \Omega }-inaccessible cardinals. Uses (presumably) Jäger's ψ.
11.^M{\displaystyle M} represents the first Mahlo cardinal. Uses Rathjen's ψ rather than Buchholz's ψ.
12.^K{\displaystyle K} represents the first weakly compact cardinal. Uses Rathjen's Ψ rather than Buchholz's ψ.
13.^Ξ{\displaystyle \Xi } represents the firstΠ02{\displaystyle \Pi _{0}^{2}}-indescribable cardinal. Uses Stegert's Ψ rather than Buchholz's ψ.
14.^Y{\displaystyle Y} is the smallestα{\displaystyle \alpha } such thatθ<Yκ<Y({\displaystyle \forall \theta <Y\exists \kappa <Y(}'κ{\displaystyle \kappa } isθ{\displaystyle \theta }-indescribable') andθ<Yκ<Y({\displaystyle \forall \theta <Y\forall \kappa <Y(}'κ{\displaystyle \kappa } isθ{\displaystyle \theta }-indescribableθ<κ{\displaystyle \rightarrow \theta <\kappa }'). Uses Stegert's Ψ rather than Buchholz's ψ.
15.^M{\displaystyle M} represents the first Mahlo cardinal. Uses (presumably) Rathjen's ψ.

Citations

[edit]
  1. ^M. Rathjen, "Admissible Proof Theory and Beyond". InStudies in Logic and the Foundations of Mathematics vol. 134 (1995), pp.123--147.
  2. ^abcRathjen,The Realm of Ordinal Analysis. Accessed 2021 September 29.
  3. ^Krajicek, Jan (1995).Bounded Arithmetic, Propositional Logic and Complexity Theory. Cambridge University Press. pp. 18–20.ISBN 9780521452052. defines the rudimentary sets and rudimentary functions, and proves them equivalent to the Δ0-predicates on the naturals. An ordinal analysis of the system can be found inRose, H. E. (1984).Subrecursion: functions and hierarchies. University of Michigan: Clarendon Press.ISBN 9780198531890.
  4. ^abcdefM. Rathjen,Proof Theory: From Arithmetic to Set Theory (p.28). Accessed 14 August 2022.
  5. ^Rathjen, Michael (2006),"The art of ordinal analysis"(PDF),International Congress of Mathematicians, vol. II, Zürich: Eur. Math. Soc., pp. 45–69,MR 2275588, archived fromthe original(PDF) on 2009-12-22, retrieved2024-05-03
  6. ^D. Madore,A Zoo of Ordinals (2017, p.2). Accessed 12 August 2022.
  7. ^"Proof-Theoretic Ordinal of ZFC or Consistent ZFC Extensions?".MathOverflow. Retrieved2026-01-23.
  8. ^Arai, Toshiyasu (2023). "Lectures on Ordinal Analysis".arXiv:2511.11196v1 [math.LO].
  9. ^abcdefgJ. Avigad, R. Sommer, "A Model-Theoretic Approach to Ordinal Analysis" (1997).
  10. ^M. Rathjen, W. Carnielli, "Hydrae and subsystems of arithmetic" (1991)
  11. ^Jeroen Van der Meeren; Rathjen, Michael; Weiermann, Andreas (2014). "An order-theoretic characterization of the Howard-Bachmann-hierarchy".arXiv:1411.4481 [math.LO].
  12. ^abcdefghijkG. Jäger, T. Strahm, "Second order theories with ordinals and elementary comprehension". Archive for Mathematical Logic vol. 34 (1995).
  13. ^abH. M. Friedman, S. G. Simpson, R. L. Smith, "Countable algebra and set existence axioms". Annals of Pure and Applied Logic vol. 25, iss. 2 (1983).
  14. ^Follows from theorem IX.4.4 of S. G. Simpson,Subsystems of Second-Order Arithmetic (2009).
  15. ^abcdeG. Jäger, "The Strength of Admissibility Without Foundation". Journal of Symbolic Logic vol. 49, no. 3 (1984).
  16. ^B. Afshari, M. Rathjen, "Ordinal Analysis and the Infinite Ramsey Theorem". In Lecture Notes in Computer Science vol. 7318 (2012)
  17. ^abMarcone, Alberto; Montalbán, Antonio (2011). "The Veblen functions for computability theorists".The Journal of Symbolic Logic.76 (2):575–602.arXiv:0910.5442.doi:10.2178/jsl/1305810765.S2CID 675632.
  18. ^S. Feferman, "Theories of finite type related to mathematical practice". InHandbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics vol. 90 (1977), ed. J. Barwise, pub. North Holland.
  19. ^abcdM. Heissenbüttel, "Theories of ordinal strengthφ20{\displaystyle \varphi 20} andφ2ε0{\displaystyle \varphi 2\varepsilon _{0}}" (2001)
  20. ^abcdefgD. Probst, "A modular ordinal analysis of metapredicative subsystems of second-order arithmetic" (2017)
  21. ^abcdF. Ranzi,From a Flexible Type System to Metapredicative Wellordering Proofs. Doctoral thesis, University of Bern, 2015.
  22. ^A. Cantini, "On the relation between choice and comprehension principles in second order arithmetic", Journal of Symbolic Logic vol. 51 (1986), pp. 360--373.
  23. ^abcdFischer, Martin; Nicolai, Carlo; Pablo Dopico Fernandez (2020). "Nonclassical truth with classical strength. A proof-theoretic analysis of compositional truth over HYPE".arXiv:2007.07188 [math.LO].
  24. ^abcS. G. Simpson, "Friedman's Research on Subsystems of Second Order Arithmetic". InHarvey Friedman's Research on the Foundations of Mathematics, Studies in Logic and the Foundations of Mathematics vol. 117 (1985), ed. L. Harrington, M. Morley, A. Šcedrov, S. G. Simpson, pub. North-Holland.
  25. ^J. Avigad, "An ordinal analysis of admissible set theory using recursion on ordinal notations".Journal of Mathematical Logic vol. 2, no. 1, pp.91--112 (2002).
  26. ^S. Feferman, "Iterated inductive fixed-point theories: application fo Hancock's conjecture". InPatras Logic Symposion, Studies in Logic and the Foundations of Mathematics vol. 109 (1982).
  27. ^S. Feferman, T. Strahm, "The unfolding of non-finitist arithmetic", Annals of Pure and Applied Logic vol. 104, no.1--3 (2000), pp.75--96.
  28. ^S. Feferman, G. Jäger, "Choice principles, the bar rule and autonomously iterated comprehension schemes in analysis", Journal of Symbolic Logic vol. 48, no. (1983), pp.63--70.
  29. ^abcdefghU. Buchholtz, G. Jäger, T. Strahm, "Theories of proof-theoretic strengthψ(ΓΩ+1){\displaystyle \psi (\Gamma _{\Omega +1})}". InConcepts of Proof in Mathematics, Philosophy, and Computer Science (2016), ed. D. Probst, P. Schuster. DOI 10.1515/9781501502620-007.
  30. ^T. Strahm, "Autonomous fixed point progressions and fixed point transfinite recursion" (2000). InLogic Colloquium '98, ed. S. R. Buss, P. Hájek, and P. Pudlák . DOI10.1017/9781316756140.031
  31. ^G. Jäger, T. Strahm, "Fixed point theories and dependent choice". Archive for Mathematical Logic vol. 39 (2000), pp.493--508.
  32. ^abcT. Strahm, "Autonomous fixed point progressions and fixed point transfinite recursion" (2000)
  33. ^abcdC. Rüede, "Transfinite dependent choice and ω-model reflection". Journal of Symbolic Logic vol. 67, no. 3 (2002).
  34. ^abcC. Rüede, "The proof-theoretic analysis of Σ11 transfinite dependent choice". Annals of Pure and Applied Logic vol. 122 (2003).
  35. ^abcdT. Strahm, "Wellordering Proofs for Metapredicative Mahlo". Journal of Symbolic Logic vol. 67, no. 1 (2002)
  36. ^F. Ranzi, T. Strahm, "A flexible type system for the small Veblen ordinal" (2019). Archive for Mathematical Logic 58: 711–751.
  37. ^K. Fujimoto, "Notes on some second-order systems of iterated inductive definitions andΠ11{\displaystyle \Pi _{1}^{1}}-comprehensions and relevant subsystems of set theory". Annals of Pure and Applied Logic, vol. 166 (2015), pp. 409--463.
  38. ^abcG. Jäger, T. Strahm, "The proof-theoretic analysis of the Suslin operator in applicative theories". InReflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman (2002).
  39. ^abcKrombholz, Martin; Rathjen, Michael (2019). "Upper bounds on the graph minor theorem".arXiv:1907.00412 [math.LO].
  40. ^W. Buchholz, S. Feferman, W. Pohlers, W. Sieg,Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies
  41. ^W. Buchholz,Proof Theory of Impredicative Subsystems of Analysis (Studies in Proof Theory, Monographs, Vol 2 (1988)
  42. ^abcdefghijklmnoM. Rathjen, "Investigations of Subsystems of Second Order Arithmetic and Set Theory in Strength betweenΠ11CA{\displaystyle \Pi _{1}^{1}{\mathsf {-CA}}} andΔ21CA+BI{\displaystyle \Delta _{2}^{1}{\mathsf {-CA+BI}}}: Part I". Archived 7 December 2023.
  43. ^M. Rathjen, "The Strength of Some Martin-Löf Type Theories"
  44. ^See conservativity result inRathjen (1996),"The Recursively Mahlo Property in Second Order Arithmetic",Mathematical Logic Quarterly,42:59–66,doi:10.1002/malq.19960420106 giving same ordinal asKPM{\displaystyle {\mathsf {KPM}}}
  45. ^abA. Setzer, "A Model for a type theory with Mahlo universe" (1996).
  46. ^M. Rathjen, "Proof Theory of Reflection". Annals of Pure and Applied Logic vol. 68, iss. 2 (1994), pp.181--224.
  47. ^abStegert, Jan-Carl, "Ordinal Proof Theory of Kripke-Platek Set Theory Augmented by Strong Reflection Principles" (2010).
  48. ^abcArai, Toshiyasu (2023-04-01). "Lectures on Ordinal Analysis".arXiv:2304.00246 [math.LO].
  49. ^Arai, Toshiyasu (2023-04-07). "Well-foundedness proof forΠ11{\displaystyle \Pi _{1}^{1}}-reflection".arXiv:2304.03851 [math.LO].
  50. ^abcArai, Toshiyasu (2024-02-12). "An ordinal analysis ofΠN{\displaystyle \Pi _{N}}-Collection".arXiv:2311.12459 [math.LO].
  51. ^Blot, Valentin (2022-08-02)."A direct computational interpretation of second-order arithmetic via update recursion".Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science. ACM. pp. 1–11.doi:10.1145/3531130.3532458.ISBN 978-1-4503-9351-5.
  52. ^Lubarsky, Robert (2015-10-02). "The Veblen functions for computability theorists".The Journal of Symbolic Logic.76 (2):575–602.arXiv:1510.00469.doi:10.2178/jsl/1305810765.

References

[edit]
Retrieved from "https://en.wikipedia.org/w/index.php?title=Ordinal_analysis&oldid=1334358662"
Categories:
Hidden categories:

[8]ページ先頭

©2009-2026 Movatter.jp