nLab
ordinal analysis

Contents

Contents

Idea

An ordinal analysis of a formal system precisely measures its proof-theoretic strength, which is its strength at justifying transfinite induction. In practice, it also measures the system’s ability to prove totality of complex computable functions.

Giving a concrete “ordinal notation” that describes the proof-theoretic strength of a system is sometimes seen as providing a constructive justification for the reasoning principles of the system. However, ordinal analysis is not limited to systems that are constructive in the sense of not assuming excluded middle. But in practice, classical systems with ordinal notations are interpretable constructively.

Relation to Predicativity

While it is classically true that any effective formal system has some limit to its proof-theoretic strength, only systems of limited strength have had their strength concretely described by a good ordinal notation. Specifically, all systems with ordinal analyses so far are significantly weaker than full second-order arithmetic. Consequently, so far, systems that have been given ordinal notations feel more like predicative systems than like familiar impredicative systems such as ZFC, higher-order arithmetic, and ETCS.

Many have argued, however, that the boundary between predicatively-justifiable and impredicative systems lies somewhere within the range of proof-theoretic ordinals already analyzed. In other words, that the stronger systems in the table below are actually slightly impredicative, even when it isn’t obvious.

Definition

Definition

The proof-theoretic ordinal of a theory TT is (commonly) defined as

|T|=sup{otyp()is primitive recursive andTTI(,X)} {\vert T\vert} = \sup\{ \mathrm{otyp}({\prec}) \mid {\prec}\text{is primitive recursive and}\; T \vdash \mathrm{TI}({\prec},X) \}

where otyp()\mathrm{otyp}({\prec}) is the order-type of the well-order \prec and TI(,X)\mathrm{TI}({\prec},X) means that XX (a free parameter) satisfies transfinite induction along \prec; this is the constructive way to say that \prec is well-ordered. For most theories, this ordinal is equal to the Π 1 1\Pi^1_1-ordinal of the theory,

|T| Π 1 1:=sup{tc(F)Fis aΠ 1 1-sentence and TF} {\vert T\vert}_{\Pi^1_1} := \sup\{ \mathrm{tc}(F) \mid F\;\text{is a}\;\Pi^1_1\text{-sentence and }\; T \vdash F \}

where tc(F)\mathrm{tc}(F) is the truth-complexity of the Π 1 1\Pi^1_1-sentence FF (if TT is a first-order theory, we interpret TX.F(X)T \vdash \forall X.F(X) as TF(X)T \vdash F(X) with a free set parameter XX).

The proof-theoretic ordinal is always a recursive ordinal (<ω 1 CK\lt\omega_1^{\mathrm{CK}}) if the theory is recursive.

Note that the proof-theoretic ordinal is a rather blunt invariant, because if FF is any true Σ 1 1\Sigma^1_1-sentence, then

|T| Π 1 1=|T+F| Π 1 1 {\vert T\vert}_{\Pi^1_1} = {\vert T+F\vert}_{\Pi^1_1}

So this tells us nothing about the provable arithmetical sentences of TT! And indeed, all true arithmetical sentences have truth-complexity less than ω\omega.

The solution is to refine the analysis to give a Π 2 0\Pi^0_2 ordinal analysis of the theory, using a measure of the computational complexity of provable Π 2 0\Pi^0_2-sentences/provably recursive functions. However, there’s no natural hierarchy of all subrecursive functions. We can define such a computational complexity depending on a choice of starting function and a choice of ordinal notation system (indeed, the Π 2 0\Pi^0_2 ordinal should be thought of as an ordinal notation, rather than an actual ordinal). But for all the ordinal analyses we have so far, these choices turn out not to matter, basically because any natural ordinal notation system will give the same result. A major issue is, however, that we have no definition of what a natural ordinal notation system is (but we know one when we see it!).

All of the ordinal analyses mentioned below also give a Π 2 0\Pi^0_2 ordinal analysis, and thus control of the computational complexity of the provably recursive functions.

Methods

Upper bounds

Most ordinal analyses proceed by embedding the theory in an infinitary proof calculus deriving judgments ρ αF\vdash^\alpha_\rho F meaning FF has an infinitary derivation of height less than α\alpha using only cuts of rank less than ρ\rho, or some refinement of such, for instance using operator controlled derivations. Then one analyzes how the height of a derivation changes during cut-elimination. For predicative theories, we’ll have

ρ αΔ 0 φραΔ \vdash^\alpha_\rho \Delta \Rightarrow \vdash^{\varphi\rho\alpha}_0 \Delta

One sets up the calculus so that 0 αF\vdash^\alpha_0 F implies tc(F)<α\mathrm{tc}(F)\lt\alpha, so this yields upper bounds for the proof-theoretic ordinal.

Lower bounds

Lower bounds are usually done by directly deriving TTI( n,X)T \vdash \mathrm{TI}({\prec_n},X) for a sequence of primitive recursive well-orderings n\prec_n whose order-types approximate the proof-theoretic ordinal. We get these primitive recursive well-orderings from good ordinal notation systems, see below.

Table of Ordinal Analyses

See below for explanations.

OrdinalFOASOAOther
Finitist systems
ω 3\omega^3EFARCA0*_0^*
ω ω\omega^\omegaPRA,IΣ 1\Sigma_1RCA0_0, WKL0_0CPRC
Predicative systems
ε 0=φ(1,0)\varepsilon_0=\varphi(1,0)PAACA0_0, Δ 1 1\Delta_1^1-CA0_0, Σ 1 1\Sigma^1_1-AC0_0EM0_0
φ(1,ε 0)\varphi(1,\varepsilon_0)ACA
φ(ω,0)\varphi(\omega,0)ID1#_1^#Δ 1 1\Delta_1^1-CREM0_0+JR
φ(ε 0,0)\varphi(\varepsilon_0,0)ID^ 1\widehat{\mathrm{ID}}_1Δ 1 1\Delta_1^1-CA, Σ 1 1\Sigma^1_1-ACEM0_0+J, ML1_1
Γ 0=φ(1,0,0)\Gamma_0=\varphi(1,0,0)ID^ <ω\widehat{\mathrm{ID}}_{\lt\omega}, U(PA)ATR0_0,Δ 1 1\Delta^1_1-CA+BRML<ω_{\lt\omega}, MLU, KPi0^0
Meta-predicative systems
φ(1,0,ε 0)\varphi(1,0,\varepsilon_0)ID^ ω\widehat{\mathrm{ID}}_{\omega}ATRKPl0^0+F-Iω_\omega
φ(1,ω,0)\varphi(1,\omega,0)ID^ <ω ω\widehat{\mathrm{ID}}_{\lt\omega^\omega}ATR0_0+(Σ 1 1\Sigma^1_1-DC)KPi0^0+Σ 1\Sigma_1-Iω_\omega
φ(1,ε 0,0)\varphi(1,\varepsilon_0,0)ID^ <ε 0\widehat{\mathrm{ID}}_{\lt\varepsilon_0}ATR+(Σ 1 1\Sigma^1_1-DC)KPi0^0+F-Iω_\omega
φ(1,Γ 0,0)\varphi(1,\Gamma_0,0)ID^ <Γ 0\widehat{\mathrm{ID}}_{\lt\Gamma_0}MLS
φ(2,0,0)\varphi(2,0,0)Aut(ID^\widehat{\mathrm{ID}})KPh0^0
φ(ω,0,0)\varphi(\omega,0,0)KPm0^0
Inductive types
ψ Ω(ε Ω+1)\psi_\Omega(\varepsilon_{\Omega+1})ID1_1KPω\omega, CZF, ML1_1V
ψ Ω(Γ Ω+1)\psi_\Omega(\Gamma_{\Omega+1})U(ID1_1)
ψ Ω(Ω ω)\psi_\Omega(\Omega_\omega)ID<ω_{\lt\omega}Π 1 1\Pi^1_1-CA0_0,Δ 2 1\Delta^1_2-CA0_0
ψ Ω(Ω ωε 0)\psi_\Omega(\Omega_\omega \varepsilon_0)W-IDω_\omegaΠ 1 1\Pi^1_1-CAW-KPl
ψ Ω(ε Ω ω+1)\psi_\Omega(\varepsilon_{\Omega_\omega+1})IDω_\omegaΠ 1 1\Pi^1_1-CA+BIKPl
ψ Ω(Ω ω ω)\psi_\Omega(\Omega_{\omega^\omega})ID<ω ω_{\lt\omega^\omega}Δ 2 1\Delta^1_2-CR
ψ Ω(Ω ε 0)\psi_\Omega(\Omega_{\varepsilon_0})ID<ε 0_{\lt\varepsilon_0}Δ 2 1\Delta^1_2-CA, Σ 2 1\Sigma^1_2-ACW-KPi
ψ Ω(ε I+1)\psi_\Omega(\varepsilon_{I+1})Δ 2 1\Delta^1_2-CA+BI, Σ 2 1\Sigma^1_2-AC+BIKPi, T0_0, CZF+REA
ψ Ω(Ω I+ω)\psi_\Omega(\Omega_{I+\omega})ML1_1W
ψ Ω(Ω L)\psi_\Omega(\Omega_L)KPh, ML<ω_{\lt\omega}W
Inductive-recursive types
ψ Ω(ε M+1)\psi_\Omega(\varepsilon_{M+1})Δ 2 1\Delta^1_2-CA+BI+(M)CZFM, KPm
ψ Ω(Ω M+ω)\psi_\Omega(\Omega_{M+\omega})KPM+^+, MLM, “Agda”

The sections of the table corresponds roughly to the kinds of reasoning captured by the systems:

  • Finitistic reasoning about the natural numbers (and other finitistic inductive types)
  • Predicative reasoning about the natural numbers
  • Meta-predicative reasoning about the natural numbers
  • Reasoning about general inductive types
  • Reasoning about general inductive-recursive types

Note that these are all very much weaker than full second-order arithmetic, and of course much weaker than Zermelo or Zermolo-Fraenkel set theory.

After the meta-predicative systems, all ordinals use a notation which refers to a much larger ordinal, often patterned on a large cardinal.

Rathjen (2005) analyzed systems up to Δ 2 1\Delta^1_2-CA+BI+Π 2 1\Pi^1_2-CA^- (the last part is parameter-free Π 2 1\Pi^1_2-comprehension), corresponding to a stable ordinal, Arai has work on a bit stronger systems, up to about Σ 4 1\Sigma^1_4-DC, in terms of ordinal diagrams defined in terms of iterated stability.

With current technology, we are very far from having ordinal analyses of stronger systems such as full second order arithmetic, ZFC set theory, or impredicative type theories such as the calculus of (inductive) constructions.

Ordinal notations

  • φ\varphi is either the binary or the ternary Veblen function
  • Ω=Ω 1\Omega=\Omega_1 is the first recursively admissible ordinal
  • Ω ξ\Omega_\xi is the ξ\xith recursively admissible ordinal
  • II is the first recursively inaccessible ordinal
  • LL is the limit of the first ω\omega recursively inaccessible ordinals
  • MM is the first recursively Mahlo ordinal

The ψ\psi functions are ordinal collapsing functions.

Systems of first-order arithmetic (FOA)

These assert some hierarchy of inductive defined sets of natural numbers.

  • EFA is elementary function arithmetic
  • PRA is primitive recursive arithmetic
  • PA is first-order Peano arithmetic
  • ID^ ν\widehat{\mathrm{ID}}_\nu extends PA by ν\nu iterated fixed points of monotone operators (not necessarily least).
  • ID1#_1^# is ID^ 1\widehat{\mathrm{ID}}_1 with induction only for positive formulas.
  • IDν_\nu, the theory of ν\nu-times iterated inductive definitions, extends PA by ν\nu iterated least fixed points of monotone operators.

Many of the results in the table concerning these can be summarized as

|ID ν|=ψ Ω(ε Ω ν+1) {\vert \mathrm{ID}_\nu \vert} = \psi_\Omega(\varepsilon_{\Omega_\nu+1})

For any of these, we get the same proof-theoretic ordinal whether we use classical or intuitionistic logic. For the IDν_\nu-systems, this is due to Sieg.

The unfolding systems U(PA) and U(ID1_1) are not exactly first-order arithmetic systems, but capture what we can get by predicative reasoning based on the natural numbers or one generalized inductive definition, respectively.

Systems of second-order arithmetic (SOA)

  • Comprehension or choice principles.
  • RCA0*_0^* is the second-order version of EFA: exp\exp is a function symbol.
  • WKL is weak König’s lemma.
  • BR is the bar induction rule.
  • BI is the bar induction axiom.
  • ATR is arithmetical transfinite recursion.
  • (M) says every true Π 3 1\Pi^1_3 sentence with parameters holds in a β\beta-model of Δ 2 1\Delta^1_2-CA.

A zero subscript indicates that we have the induction axiom rather than the induction scheme, except for RCA0_0 which has the Σ 1 0\Sigma^0_1-induction scheme.

Kripke Platek Set theories

  • KPω\omega is Kripke-Platek set theory, whose universe is an admissible set containing ω\omega.
  • KPl asserts that the universe is a limit of admissible sets
  • KPi asserts that the universe is inaccessible sets
  • KPh asserts that the universe is hyperinaccessible: a limit of inaccessible sets
  • KPm asserts that the universe is a Mahlo set

A superscript zero indidcates that \in-induction is removed.

About the Mahlo level: this also corresponds to inductive-recursive definitions (Dybjer-Setzer).

Martin-Löf type theories

  • CPRC is the Herbelin-Patey Calculus of Primitive Recursive Constructions.
  • MLn_n is type theory without W-types with nn universes.
  • ML<ω_{\lt\omega} is type theory without W-types with an infinite hierarchy of universes.
  • MLU is type theory with a next universe operator.
  • MLS is type theory without W-types with a superuniverse.
  • ML1_1V is type theory with one universe and Aczel’s type of iterative sets.
  • ML1_1W is type theory with W-types and one universe.
  • ML<ω_{\lt\omega}W is type theory with W-types and an infinite hierarchy of universes (this corresponds to the type theory in Lean’s HoTT mode).
  • MLM is Martin-Löf type theory with a Mahlo universe.

Constructive Set theories

  • CZF is Aczel’s constructive set theory.
  • REA is the regular extension axiom.
  • CZFM is CZF with a Mahlo universe

Explicit mathematics systems

  • EM0_0 is basic explicit mathematics with elementary comprehension
  • JR is the join rule, J is the join axioms
  • T0_0 is EM0_0+J+IG, where IG is inductive generation

References

  • Aczel, The Type Theoretic Interpretation of Constructive Set Theory, Logic Colloquium 1977.

  • Arai, A sneak preview of proof theory of ordinals, arXiv 1102.0596.

  • Arai, Proof theory for theories of ordinals III: Π N\Pi_N-reflection, arXiv 1007.0844.

  • Buchholz, A simplified version of local predicativity, Proc. Proof Theory Meeting Leed ‘90.

  • Buchholz, A Note on the Ordinal Analysis of KPM (2002).

  • Buchholz, Feferman, Pohlers and Sieg, Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies, Lecture Notes in Mathematics 897 (1981).

  • Dybjer and Setzer, Induction-recursion and initial algebras, APAL 124(1-3), 2003, pp. 1-47. DOI: 10.1016/S0168-0072(02)00096-9

  • Feferman: Iterated inductive fixed-point theories: Application to Hancock’s conjecture, in: G. Metakides (ed.): Patras Logic Symposium (North-Holland, Amsterdam, (1982), 171–196.

  • Jäger, Kahle, Setzer, and Strahm, The proof-theoretic analysis of transfinitely iterated fixed point theories, Journal of Symbolic Logic

  • Jäger and Strahm, Fixed point theories and dependent choice. Archive for Mathematical Logic.

  • Rathjen, Ordinal notations based on a weakly Mahlo cardinal, Archive for Mathematical Logic 29 (1990), 249-263.

  • Rathjen, Proof-theoretic analysis of KPm, Archive for Mathematical Logic (1991).

  • Rathjen, The Recursively Mahlo Property in Second Order Arithmetic, Mathematical Logic Quarterly 42 (1996), 59-66.

  • Rathjen, The strength of Martin-Löf type theory with a superuniverse. Part II, 2001, AML, DOI: 10.1007/s001530000051

  • Rathjen, The strength of Martin-Löf type theory with a superuniverse. Part I, 2000, AML, DOI: 10.1007/s001530050001

  • Rathjen, An ordinal analysis of parameter free Π 2 1\Pi^1_2-comprehension. Arch. Math. Log. 44(3), 263–362 (2005).

  • Rathjen, The constructive Hilbert program and the limits of Martin-Löf type theory (2005), Synthese, DOI: 10.1007/s11229-004-6208-4

  • Rathjen, Griffor and Palmgren, Inaccessibility in Constructive Set Theory and Type Theory, APAL 94 (1998), 181-200.

  • Setzer, An upper bound for the proof theoretical strength of Martin-Löf Type Theory with W-type and one universe (2006)

  • Strahm, Autonomous fixed point progressions and fixed point transfinite recursion, Proc. of Logic Colloquium ‘98, 449-464, web

Last revised on October 1, 2019 at 09:20:11. See the history of this page for a list of all contributions to it.