Bachmann–Howard ordinal
In mathematics, the Bachmann–Howard ordinal (also known as the Howard ordinal, or Howard-Bachmann ordinal) is a large countable ordinal. It is the proof-theoretic ordinal of several mathematical theories, such as  Kripke–Platek set theory (with the axiom of infinity) 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 ωε = ε.
Ω = ω1 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 (except that ψ can only be applied to arguments  less than α, to ensure that it is well defined). The Bachmann–Howard ordinal is ψ(εΩ+1). The Bachmann–Howard ordinal can also be defined as  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. References

  (Slides of a talk given at Fischbachau.) Citations

Proof theory
Ordinal numbers