Ordinal analysis - Alchetron, The Free Social Encyclopedia

In proof theory, ordinal analysis assigns ordinals (often large countable ordinals) to mathematical theories as a measure of their strength. The field was formed when Gerhard Gentzen in 1934 used cut elimination to prove, in modern terms, that the proof-theoretic ordinal of Peano arithmetic is ε₀.

Definition

Ordinal analysis concerns true, effective (recursive) theories that can interpret a sufficient portion of arithmetic to make statements about ordinal notations. The proof-theoretic ordinal of such a theory T is the smallest recursive ordinal that the theory cannot prove is well founded—the supremum of all ordinals α for which there exists a notation o in Kleene's sense such that T proves that o is an ordinal notation. Equivalently, it is the supremum of all ordinals α such that there exists a recursive relation R on ω (the set of natural numbers) that well-orders it with ordinal α and such that T proves transfinite induction of arithmetical statements for R .

The existence of any recursive ordinal that the theory fails to prove is well ordered follows from the Σ 1 1 bounding theorem, as the set of natural numbers that an effective theory proves to be ordinal notations is a Σ 1 0 set (see Hyperarithmetical theory). Thus the proof-theoretic ordinal of a theory will always be a countable ordinal less than the Church-Kleene ordinal ω 1 C K .

In practice, the proof-theoretic ordinal of a theory is a good measure of the strength of a theory. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has a larger proof-theoretic ordinal than another it can often prove the consistency of the second theory.

Theories with proof-theoretic ordinal ω2

RFA, rudimentary function arithmetic.

IΔ₀, arithmetic with induction on Δ₀-predicates without any axiom asserting that exponentiation is total.

Theories with proof-theoretic ordinal ω3

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

EFA, elementary function arithmetic.

IΔ₀ + exp, arithmetic with induction on Δ₀-predicates augmented by an axiom asserting that exponentiation is total.

RCA*
0, a second order form of EFA sometimes used in reverse mathematics.

WKL*
0, a second order form of EFA sometimes used in reverse mathematics.

Theories with proof-theoretic ordinal ωn

IΔ₀ or EFA augmented by an axiom ensuring that each element of the n-th level E n of the Grzegorczyk hierarchy is total.

Theories with proof-theoretic ordinal ωω

RCA₀, recursive comprehension.

WKL₀, weak König's lemma.

PRA, primitive recursive arithmetic.

IΣ₁, arithmetic with induction on Σ₁-predicates.

Theories with proof-theoretic ordinal ε0

PA, Peano arithmetic (shown by Gentzen using cut elimination).

ACA₀, arithmetical comprehension.

Theories with proof-theoretic ordinal the Feferman-Schütte ordinal Γ0

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

ATR₀, arithmetical transfinite recursion.

Martin-Löf type theory with arbitrarily many finite level universes.

Theories with proof-theoretic ordinal the Bachmann-Howard ordinal

ID₁, the theory of inductive definitions.

KP, Kripke-Platek set theory with the axiom of infinity.

CZF, Aczel's constructive Zermelo-Fraenkel set theory.

MLW, Martin-Löf Type Theory with indexed W-Types

EON, a weak variant of the Feferman's explicit mathematics system T₀.

Theories with larger proof-theoretic ordinals

Π 1 1 - C A 0 , Π₁¹ comprehension has a rather large proof-theoretic ordinal, which was described by Takeuti in terms of "ordinal diagrams", and which is bounded by ψ₀(Ω_ω) in Buchholz's notation. It is also the ordinal of I D < ω , the theory of finitely iterated inductive definitions.

T₀, Feferman's constructive system of explicit mathematics has a larger proof-theoretic ordinal, which is also the proof-theoretic ordinal of the KPi, Kripke-Platek Set theory with iterated admissibles and Σ 2 1 - A C + B I .

KPM, an extension of Kripke-Platek set theory based on a Mahlo cardinal, has a very large proof-theoretic ordinal ϑ, which was described by Rathjen (1990).

MLM, an extension of Martin-Löf type theory by one Mahlo-universe, has an even larger proof-theoretic ordinal ψ_Ω₁(Ω_{M + ω}).

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 (as of 2008) been given. This includes second-order arithmetic and set theories with powersets. (The CZF and Kripke-Platek set theories mentioned above are weak set theories without powersets.)

References

Ordinal analysis Wikipedia

(Text) CC BY-SA

Contents