In
proof theory, ordinal analysis assigns
ordinals (often
large countable ordinals) to mathematical theories as a measure of their strength.
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.
History
The field of ordinal analysis was formed when
Gerhard Gentzen
Gerhard Karl Erich Gentzen (24 November 1909 – 4 August 1945) was a German mathematician and logician. He made major contributions to the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus. He died ...
in 1934 used
cut elimination to prove, in modern terms, that the proof-theoretic ordinal of
Peano arithmetic is
ε0. See
Gentzen's consistency proof.
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
is the supremum of the
order types of all
ordinal notation
In mathematical logic and set theory, an ordinal notation is a partial function mapping the set of all finite sequences of symbols, themselves members of a finite alphabet, to a countable set of ordinals. A Gödel numbering is a function mapping t ...
s (necessarily
recursive
Recursion (adjective: ''recursive'') occurs when a thing is defined in terms of itself or of its type. Recursion is used in a variety of disciplines ranging from linguistics to logic. The most common application of recursion is in mathematics ...
, see next section) that the theory can prove are
well founded—the supremum of all ordinals
for which there exists a
notation in Kleene's sense such that
proves that
is an ordinal notation. Equivalently, it is the supremum of all ordinals
such that there exists a
recursive relation on
(the set of natural numbers) that
well-orders it with ordinal
and such that
proves
transfinite induction of arithmetical statements for
.
Ordinal notations
Some theories, such as subsystems of second-order arithmetic, have no conceptualization of or way to make arguments about transfinite ordinals. For example, to formalize what it means for a subsystem of Z
2 to "prove
well-ordered", we instead construct an
ordinal notation
In mathematical logic and set theory, an ordinal notation is a partial function mapping the set of all finite sequences of symbols, themselves members of a finite alphabet, to a countable set of ordinals. A Gödel numbering is a function mapping t ...
with order type
.
can now work with various transfinite induction principles along
, 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 a primitive recursive notation system
that is well-founded iff PA is consistent, despite having order type
- including such a notation in the ordinal analysis of PA would result in the false equality
.
Upper bound
For any theory that's both
-axiomatizable and
-sound, the existence of a recursive ordering that the theory fails to prove is well-ordered follows from the
bounding theorem, and said provably well-founded ordinal notations are in fact well-founded by
-soundness. Thus the proof-theoretic ordinal of a
-sound theory that has a
axiomatization will always be a (countable)
recursive ordinal In mathematics, specifically computability and set theory, an ordinal \alpha is said to be computable or recursive if there is a computable well-ordering of a subset of the natural numbers having the order type \alpha.
It is easy to check that \om ...
, that is, less than the
Church–Kleene ordinal
In mathematics, particularly set theory, non-recursive ordinals are large countable ordinals greater than all the recursive ordinals, and therefore can not be expressed using ordinal collapsing functions.
The Church–Kleene ordinal and varian ...
.
Examples
Theories with proof-theoretic ordinal ω
*Q,
Robinson arithmetic (although the definition of the proof-theoretic ordinal for such weak theories has to be tweaked).
*PA
–, the first-order theory of the nonnegative part of a discretely ordered ring.
Theories with proof-theoretic ordinal ω2
*RFA,
rudimentary function arithmetic.
[ 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 in ]
*IΔ
0, arithmetic with induction on Δ
0-predicates without any axiom asserting that exponentiation is total.
Theories with proof-theoretic ordinal ω3
*EFA,
elementary function arithmetic
In proof theory, a branch of mathematical logic, elementary function arithmetic (EFA), also called elementary arithmetic and exponential function arithmetic,C. Smoryński, "Nonstandard Models and Related Developments" (p. 217). From ''Harvey Frie ...
.
*IΔ
0 + exp, arithmetic with induction on Δ
0-predicates augmented by an axiom asserting that exponentiation is total.
*RCA, a second order form of EFA sometimes used in
reverse mathematics
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in cont ...
.
*WKL, a second order form of EFA sometimes used in
reverse mathematics
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in cont ...
.
Friedman's
grand 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'' (for ''n'' = 2, 3, ... ω)
*IΔ
0 or EFA augmented by an axiom ensuring that each element of the ''n''-th level
of the
Grzegorczyk hierarchy is total.
Theories with proof-theoretic ordinal ωω
*RCA
0,
recursive comprehension.
*WKL
0,
weak König's lemma.
*PRA,
primitive recursive arithmetic.
*IΣ
1, arithmetic with induction on Σ
1-predicates.
Theories with proof-theoretic ordinal ε0
*PA,
Peano arithmetic (
shown by
Gentzen
Gerhard Karl Erich Gentzen (24 November 1909 – 4 August 1945) was a German mathematician and logician. He made major contributions to the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus. He died o ...
using
cut elimination).
*ACA
0,
arithmetical comprehension.
Theories with proof-theoretic ordinal the Feferman–Schütte ordinal Γ0
*ATR
0,
arithmetical transfinite recursion
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in cont ...
.
*
Martin-Löf type theory with arbitrarily many finite level universes.
This ordinal is sometimes considered to be the upper limit for "predicative" theories.
Theories with proof-theoretic ordinal the Bachmann–Howard ordinal
* ID
1, the first
theory of inductive definitions.
* KP,
Kripke–Platek set theory
The Kripke–Platek set theory (KP), pronounced , is an axiomatic set theory developed by Saul Kripke and Richard Platek.
The theory can be thought of as roughly the predicative part of ZFC and is considerably weaker than it.
Axioms
In its fo ...
with the
axiom of infinity
In axiomatic set theory and the branches of mathematics and philosophy that use it, the axiom of infinity is one of the axioms of Zermelo–Fraenkel set theory. It guarantees the existence of at least one infinite set, namely a set containing th ...
.
* CZF, Aczel's
constructive Zermelo–Fraenkel set theory.
* EON, a weak variant of the
Feferman's explicit mathematics system T
0.
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
*
,
Π11 comprehension has a rather large proof-theoretic ordinal, which was described by Takeuti in terms of "ordinal diagrams", and which is bounded by
ψ0(Ωω) in
Buchholz's notation. It is also the ordinal of
, the theory of finitely iterated inductive definitions. And also the ordinal of MLW, Martin-Löf type theory with indexed W-Types .
*ID
ω, the
theory of ω-iterated inductive definitions. Its proof-theoretic ordinal is equal to the
Takeuti-Feferman-Buchholz ordinal.
*T
0, 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
.
*KPi, an extension of
Kripke–Platek set theory
The Kripke–Platek set theory (KP), pronounced , is an axiomatic set theory developed by Saul Kripke and Richard Platek.
The theory can be thought of as roughly the predicative part of ZFC and is considerably weaker than it.
Axioms
In its fo ...
based on a
recursively inaccessible ordinal, has a very large proof-theoretic ordinal
described in a 1983 paper of Jäger and Pohlers, where I is the smallest inaccessible.
[D. Madore]
A Zoo of Ordinals
(2017, p.2). Accessed 12 August 2022. This ordinal is also the proof-theoretic ordinal of
.
*KPM, an extension of
Kripke–Platek set theory
The Kripke–Platek set theory (KP), pronounced , is an axiomatic set theory developed by Saul Kripke and Richard Platek.
The theory can be thought of as roughly the predicative part of ZFC and is considerably weaker than it.
Axioms
In its fo ...
based on a
recursively Mahlo ordinal, has a very large proof-theoretic ordinal θ, which was described by .
*MLM, an extension of Martin-Löf type theory by one Mahlo-universe, has an even larger proof-theoretic ordinal ψ
Ω1(Ω
M + ω).
*
has a proof-theoretic ordinal equal to
, where
refers to the first weakly compact, using Rathjen's Psi function
*
has a proof-theoretic ordinal equal to
, where
refers to the first
-indescribable and
, using Stegert's Psi function.
*
has a proof-theoretic ordinal equal to
where
is a cardinal analogue of the least ordinal
which is
-stable for all
and
, using Stegert's Psi function.
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
, full
second-order arithmetic
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.
A precur ...
(
) and set theories with powersets including
ZF and ZFC. The strength of
intuitionistic ZF (IZF) equals that of ZF.
Table of ordinal analyses
Key
This is a list of symbols used in this table:
* ψ represents
Buchholz's psi unless stated otherwise.
* Ψ represents either Rathjen's or Stegert's Psi.
* φ represents Veblen's function.
* ω represents the first transfinite ordinal.
* ε
α represents the
epsilon numbers.
* Γ
α represents the gamma numbers (Γ
0 is the
Feferman–Schütte ordinal)
* Ω
α represent the uncountable ordinals (Ω
1, abbreviated Ω, is
ω1).
This is a list of the abbreviations used in this table:
* First-order arithmetic
**
is
Robinson arithmetic
**
is the first-order theory of the nonnegative part of a discretely ordered ring.
**
is
rudimentary function arithmetic.
**
is arithmetic with induction restricted to Δ
0-predicates without any axiom asserting that exponentiation is total.
**
is
elementary function arithmetic
In proof theory, a branch of mathematical logic, elementary function arithmetic (EFA), also called elementary arithmetic and exponential function arithmetic,C. Smoryński, "Nonstandard Models and Related Developments" (p. 217). From ''Harvey Frie ...
.
**
is arithmetic with induction restricted to Δ
0-predicates augmented by an axiom asserting that exponentiation is total.
**
is elementary function arithmetic augmented by an axiom ensuring that each element of the ''n''-th level
of the
Grzegorczyk hierarchy is total.
**
is
augmented by an axiom ensuring that each element of the ''n''-th level
of the
Grzegorczyk hierarchy is total.
**
is
primitive recursive arithmetic.
**
is arithmetic with induction restricted to Σ
1-predicates.
**
is
Peano arithmetic.
**
is
but with induction only for positive formulas.
**
extends PA by ν iterated fixed points of monotone operators.
**
is not exactly a first-order arithmetic system, but captures what one can get by predicative reasoning based on the natural numbers.
**
is an
automorphism on
.
**
extends PA by ν iterated least fixed points of monotone operators.
**
is not exactly a first-order arithmetic system, but captures what one can get by predicative reasoning based on ν-times iterated generalized inductive definitions.
**
is an automorphism on
.
**
is a weakened version of
based on W-types.
* Second-order arithmetic
**
is a second order form of
sometimes used in
reverse mathematics
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in cont ...
.
**
is a second order form of
sometimes used in reverse mathematics.
**
is
recursive comprehension.
**
is
weak König's lemma.
**
is
arithmetical comprehension.
**
is
plus the full second-order induction scheme.
**
is
arithmetical transfinite recursion
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in cont ...
.
**
is
plus the full second-order induction scheme.
**
is
plus the assertion ''"every true
-sentence with parameters holds in a (countable coded)
-model of
".''
* Kripke-Platek set theory
**
is
Kripke-Platek set theory with the axiom of infinity.
**
is Kripke-Platek set theory, whose universe is an admissible set containing
.
**
is a weakened version of
based on W-types.
**
asserts that the universe is a limit of admissible sets.
**
is a weakened version of
based on W-types.
**
asserts that the universe is inaccessible sets.
**
asserts that the universe is hyperinaccessible: an inaccessible set and a limit of inaccessible sets.
**
asserts that the universe is a Mahlo set.
**
is
augmented by a certain first-order reflection scheme.
**
is KPi augmented by the axiom
.
**
is KPI augmented by the assertion ''"at least one recursively Mahlo ordinal exists".''
A superscript zero indicates that
-induction is removed (making the theory significantly weaker).
* Type theory
**
is the Herbelin-Patey Calculus of Primitive Recursive Constructions.
**
is type theory without W-types and with
universes.
**
is type theory without W-types and with finitely many universes.
**
is type theory with a next universe operator.
**
is type theory without W-types and with a superuniverse.
**
is an automorphism on type theory without W-types.
**
is type theory with one universe and Aczel's type of iterative sets.
**
is type theory with indexed W-Types.
**
is type theory with W-types and one universe.
**
is type theory with W-types and finitely many universes.
**
is an automorphism on type theory with W-types.
**
is type theory with a Mahlo universe.
* Constructive set theory
**
is Aczel's constructive set theory.
**
is
plus the regular extension axiom.
**
is
plus the full-second order induction scheme.
**
is
with a Mahlo universe.
* Explicit mathematics
**
is basic explicit mathematics plus elementary comprehension
**
is
plus join rule
**
is
plus join axioms
**
is a weak variant of the
Feferman's
.
**
is
, where
is inductive generation.
**
is
, where
is the full second-order induction scheme.
See also
*
Equiconsistency
*
Large cardinal property
In the mathematical field of set theory, a large cardinal property is a certain kind of property of transfinite cardinal numbers. Cardinals with such properties are, as the name suggests, generally very "large" (for example, bigger than the least ...
*
Feferman–Schütte ordinal
*
Bachmann–Howard ordinal
*
Complexity class
*
Gentzen's consistency proof
Notes
:1.For
:2.The Veblen function
with countably infinitely iterated least fixed points.
:3.Can also be commonly written as
in Madore's ψ.
:4.Uses Madore's ψ rather than Buchholz's ψ.
:5.Can also be commonly written as
in Madore's ψ.
:6.
represents the first recursively weakly compact ordinal. Uses Arai's ψ rather than Buchholz's ψ.
:7.Also the proof-theoretic ordinal of
, as the amount of weakening given by the W-types is not enough.
:8.
represents the first inaccessible cardinal. Uses Jäger's ψ rather than Buchholz's ψ.
:9.
represents the limit of the
-inaccessible cardinals. Uses (presumably) Jäger's ψ.
:10.
represents the limit of the
-inaccessible cardinals. Uses (presumably) Jäger's ψ.
:11.
represents the first Mahlo cardinal. Uses Rathjen's ψ rather than Buchholz's ψ.
:12.
represents the first weakly compact cardinal. Uses Rathjen's Ψ rather than Buchholz's ψ.
:13.
represents the first
-indescribable cardinal. Uses Stegert's Ψ rather than Buchholz's ψ.
:14.
is the smallest
such that
'
is
-indescribable') and
'
is
-indescribable
'). Uses Stegert's Ψ rather than Buchholz's ψ.
:15.
represents the first Mahlo cardinal. Uses (presumably) Rathjen's ψ.
Citations
References
*
*
*
*
*
*
*
*
*{{citation, mr=0882549, last= Takeuti, first= Gaisi , title=Proof theory, edition= Second , series= Studies in Logic and the Foundations of Mathematics, volume= 81, publisher= North-Holland Publishing Co., place= Amsterdam, year=1987, isbn= 0-444-87943-9
Proof theory
Ordinal numbers