Bachmann–Howard ordinal

In mathematics, the Bachmann–Howard ordinal is a large countable ordinal.
It is the proof-theoretic ordinal of several mathematical theories, such as Kripke–Platek set theory and the system CZF of constructive set theory.
It was introduced by and.

Definition

The Bachmann–Howard ordinal is defined using an ordinal collapsing function:

ε_α enumerates the epsilon numbers, the ordinals ε such that ω^ε = ε.
Ω = ω₁ is the first uncountable ordinal.
ε_Ω+1 is the first epsilon number after Ω = ε_Ω.
ψ is defined to be the smallest ordinal that cannot be constructed by starting with 0, 1, ω and Ω, and repeatedly applying ordinal addition, multiplication and exponentiation, and ψ to previously constructed ordinals.
The Bachmann–Howard ordinal is ψ.

The Bachmann–Howard ordinal can also be defined as φ_{ε_Ω+1} for an extension of the Veblen functions φ_α to certain functions α of ordinals; this extension was carried out by Heinz Bachmann and is not completely straightforward.