Bachmann–Howard ordinal

Last updated • 1 min readFrom Wikipedia, The Free Encyclopedia

In mathematics, the Bachmann–Howard ordinal (also known as the Howard ordinal, or Howard-Bachmann ordinal [1] ) 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 HeinzBachmann  ( 1950 ) and William AlvinHoward  ( 1972 ).

Contents

Definition

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

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. [2] [3]

Citations

  1. J. Van der Meeren, M. Rathjen, A. Weiermann, An order-theoretic characterization of the Howard-Bachmann-hierarchy (2017). Accessed 21 February 2023.
  2. S. Feferman, The proof theory of classical and constructive inductive definitions. A 40 year saga, 1968-2008. (2008), p.7. Accessed 21 February 2023.
  3. M. Rathjen, The Art of Ordinal Analysis (2006), p.11. Accessed 21 February 2023.

Related Research Articles

An infinitary logic is a logic that allows infinitely long statements and/or infinitely long proofs. The concept was introduced by Zermelo in the 1930s.

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.

In mathematics, the epsilon numbers are a collection of transfinite numbers whose defining property is that they are fixed points of an exponential map. Consequently, they are not reachable from 0 via a finite series of applications of the chosen exponential map and of "weaker" operations like addition and multiplication. The original epsilon numbers were introduced by Georg Cantor in the context of ordinal arithmetic; they are the ordinal numbers ε that satisfy the equation

In the mathematical discipline of set theory, there are many ways of describing specific countable ordinals. The smallest ones can be usefully and non-circularly expressed in terms of their Cantor normal forms. Beyond that, many ordinals of relevance to proof theory still have computable ordinal notations. However, it is not possible to decide effectively whether a given putative ordinal notation is a notation or not ; various more-concrete ways of defining ordinals that definitely have notations are available.

In set theory, an ordinal number α is an admissible ordinal if Lα is an admissible set ; in other words, α is admissible when α is a limit ordinal and Lα ⊧ Σ0-collection. The term was coined by Richard Platek in 1966.

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 the set of well-formed formulae of some formal language to the natural numbers. This associates each well-formed formula with a unique natural number, called its Gödel number. If a Gödel numbering is fixed, then the subset relation on the ordinals induces an ordering on well-formed formulae which in turn induces a well-ordering on the subset of natural numbers. A recursive ordinal notation must satisfy the following two additional properties:

  1. the subset of natural numbers is a recursive set
  2. the induced well-ordering on the subset of natural numbers is a recursive relation

In proof theory, ordinal analysis assigns 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.

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 recursive ordinal notations.

In mathematics, the Feferman–Schütte ordinal Γ0 is a large countable ordinal. It is the proof-theoretic ordinal of several mathematical theories, such as arithmetical transfinite recursion. It is named after Solomon Feferman and Kurt Schütte, the former of whom suggested the name Γ0.

In mathematics, the small Veblen ordinal is a certain large countable ordinal, named after Oswald Veblen. It is occasionally called the Ackermann ordinal, though the Ackermann ordinal described by Ackermann (1951) is somewhat smaller than the small Veblen ordinal.

In mathematics, the Veblen functions are a hierarchy of normal functions, introduced by Oswald Veblen in Veblen (1908). If φ0 is any normal function, then for any non-zero ordinal α, φα is the function enumerating the common fixed points of φβ for β<α. These functions are all normal.

In mathematical logic and set theory, an ordinal collapsing function is a technique for defining certain recursive large countable ordinals, whose principle is to give names to certain ordinals much larger than the one being defined, perhaps even large cardinals, and then "collapse" them down to a system of notations for the sought-after ordinal. For this reason, ordinal collapsing functions are described as an impredicative manner of naming ordinals.

In mathematics, ψ0ω), widely known as Buchholz's ordinal, is a large countable ordinal that is used to measure the proof-theoretic strength of some mathematical systems. In particular, it is the proof theoretic ordinal of the subsystem -CA0 of second-order arithmetic; this is one of the "big five" subsystems studied in reverse mathematics (Simpson 1999). It is also the proof-theoretic ordinal of , the theory of finitely iterated inductive definitions, and of , a fragment of Kripke-Platek set theory extended by an axiom stating every set is contained in an admissible set. Buchholz's ordinal is also the order type of the segment bounded by in Buchholz's ordinal notation . Lastly, it can be expressed as the limit of the sequence: , , , ...

In computability theory, computational complexity theory and proof theory, a fast-growing hierarchy is an ordinal-indexed family of rapidly increasing functions fα: NN. A primary example is the Wainer hierarchy, or Löb–Wainer hierarchy, which is an extension to all α < ε0. Such hierarchies provide a natural way to classify computable functions according to rate-of-growth and computational complexity.

In computability theory, computational complexity theory and proof theory, the slow-growing hierarchy is an ordinal-indexed family of slowly increasing functions gα: NN. It contrasts with the fast-growing hierarchy.

In the mathematical fields of set theory and proof theory, the Takeuti–Feferman–Buchholz ordinal (TFBO) is a large countable ordinal, which acts as the limit of the range of Buchholz's psi function and Feferman's theta function. It was named by David Madore, after Gaisi Takeuti, Solomon Feferman and Wilfried Buchholz. It is written as using Buchholz's psi function, an ordinal collapsing function invented by Wilfried Buchholz, and in Feferman's theta function, an ordinal collapsing function invented by Solomon Feferman. It is the proof-theoretic ordinal of several formal theories:

In set theory and logic, Buchholz's ID hierarchy is a hierarchy of subsystems of first-order arithmetic. The systems/theories are referred to as "the formal theories of ν-times iterated inductive definitions". IDν extends PA by ν iterated least fixed points of monotone operators.

In mathematics, Rathjen's  psi function is an ordinal collapsing function developed by Michael Rathjen. It collapses weakly Mahlo cardinals to generate large countable ordinals. A weakly Mahlo cardinal is a cardinal such that the set of regular cardinals below is closed under . Rathjen uses this to diagonalise over the weakly inaccessible hierarchy.

In set theory, a mathematical discipline, a fundamental sequence is a cofinal sequence of ordinals all below a given limit ordinal. Depending on author, fundamental sequences may be restricted to ω-sequences only or permit fundamental sequences of length . The nth element of the fundamental sequence of is commonly denoted , although it may be denoted or . Additionally, some authors may allow fundamental sequences to be defined on successor ordinals. The term dates back to Veblen's construction of normal functions , while the concept dates back to Hardy's 1904 attempt to construct a set of cardinality .

References