In mathematics, the Bachmann–Howard ordinal (also known as the Howard ordinal, or Howard–Bachmann ordinalJ. Van der Meeren, M. Rathjen, A. Weiermann, "An order-theoretic characterization of the Howard-Bachmann-hierarchy" (2017). Accessed 21 February 2023.) 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 φεΩ+1(0) 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.S. Feferman, "The proof theory of classical and constructive inductive definitions. A 40 year saga, 1968-2008." (2008), p.7. Accessed 21 February 2023.M. Rathjen, "The Art of Ordinal Analysis" (2006), p.11. Accessed 21 February 2023.
Citations
References
(Slides of a talk given at Fischbachau.)