In mathematical logic
and set theory
, an ordinal collapsing function
(or projection function
) is a technique for defining (notations
for) 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
(though they can be replaced with recursively large ordinals
at the cost of extra technical difficulty), 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.
The details of the definition of ordinal collapsing functions vary, and get more complicated as greater ordinals are being defined, but the typical idea is that whenever the notation system “runs out of fuel” and cannot name a certain ordinal, a much larger ordinal is brought “from above” to give a name to that critical point. An example of how this works will be detailed below, for an ordinal collapsing function defining the Bachmann-Howard ordinal (i.e., defining a system of notations up to the Bachmann-Howard ordinal).
The use and definition of ordinal collapsing functions is inextricably intertwined with the theory of ordinal analysis, since the large countable ordinals defined and denoted by a given collapse are used to describe the ordinal-theoretic strength of certain formal systems, typically subsystems of analysis (such as those seen in the light of reverse mathematics), extensions of Kripke-Platek set theory, Bishop-style systems of constructive mathematics or Martin-Löf-style systems of intuitionistic type theory.
Ordinal collapsing functions are typically denoted using some variation of the greek letter (psi).
An example leading up to the Bachmann-Howard ordinal
The choice of the ordinal collapsing function given as example below imitates greatly the system introduced by Buchholz but is limited to collapsing one cardinal for clarity of exposition. More on the relation between this example and Buchholz's system will be said below.
stand for the first uncountable ordinal
, or, in fact, any ordinal which is (an
-number and) guaranteed to be greater than all the countable ordinals which will be constructed (for example, the Church-Kleene ordinal
is adequate for our purposes; but we will work with
because it allows the convenient use of the word countable
in the definitions).
We define a function (which will be non-decreasing and continuous), taking an arbitrary ordinal to a countable ordinal , recursively on , as follows:
- Assume has been defined for all
- Let be the set of ordinals generated starting from , , and by recursively applying the following functions: ordinal addition, multiplication and exponentiation and the function , i.e., the restriction of to ordinals
- Then is defined as the smallest ordinal not belonging to .
In a more concise (although more obscure) way:
- is the smallest ordinal which cannot be expressed from , , and using sums, products, exponentials, and the function itself (to previously constructed ordinals less than ).
Here is an attempt to explain the motivation for the definition of in intuitive terms: since the usual operations of addition, multiplication and exponentiation are not sufficient to designate ordinals very far, we attempt to systematically create new names for ordinals by taking the first one which does not have a name yet, and whenever we run out of names, rather than invent them in an ad hoc fashion or using diagonal schemes, we seek them in the ordinals far beyond the ones we are constructing (beyond , that is); so we give names to uncountable ordinals and, since in the end the list of names is necessarily countable, will “collapse” them to countable ordinals.
Computation of values of
To clarify how the function
is able to produce notations for certain ordinals, we now compute its first values.
. It contains ordinals
and so on. It also contains such ordinals as
. The first ordinal which it does not contain is
(which is the limit of
and so on — less than
by assumption). The upper bound of the ordinals it contains is
(the limit of
and so on), but that is not so important. This shows that
Similarly, contains the ordinals which can be formed from , , , and this time also , using addition, multiplication and exponentiation. This contains all the ordinals up to but not the latter, so . In this manner, we prove that inductively on : the proof works, however, only as long as