nLab
ordinal analysis

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:

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

The ψ\psi functions are ordinal collapsing functions.

Systems of first-order arithmetic (FOA)

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

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)

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

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

Constructive Set theories

Explicit mathematics systems

References