Ordinal collapsing function: Difference between revisions

Revision as of 08:06, 29 March 2025

Latest revision as of 19:30, 26 August 2025

(2 intermediate revisions by 2 users not shown)

Line 1:

{{Short description|Set-theoretic function}}

{{No citations|date=June 2022}}

In [[mathematical logic]] and [[set theory]], an '''ordinal collapsing function''' (or '''projection function''') is a technique for defining ([[Ordinal notation|notations]] for) certain [[Recursive ordinal|recursive]] [[large countable ordinal]]s, whose principle is to give names to certain ordinals much larger than the one being defined, perhaps even [[Large cardinal property|large cardinals]] (though they can be replaced with [[Large countable ordinal#Beyond admissible ordinals|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 [[Impredicativity|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 system]]s, typically<ref name="Rathjen-survey">Rathjen, 1995 (Bull. Symbolic Logic)</ref><ref name="Kahle">Kahle, 2002 (Synthese)</ref> subsystems of [[second-order arithmetic|analysis]] (such as those seen in the light of [[reverse mathematics]]), extensions of [[Kripke–Platek set theory]], [[Errett Bishop|Bishop]]-style systems of [[Constructivism (mathematics)|constructive mathematics]] or [[Per Martin-Löf|Martin-Löf]]-style systems of [[intuitionistic type theory]].

Ordinal collapsing functions are typically denoted using some variation of either the Greek letter <math>\psi</math> ([[Psi (letter)|psi]]) or <math>\theta</math> ([[theta]]).

== An example leading up to the Bachmann–Howard ordinal ==

Line 67:

==== A note about base representations ====

Recall that if <math>\delta</math> is an ordinal which is a power of <math>\omega</math> (for example <math>\omega</math> itself, or <math>\varepsilon_0</math>, or <math>\Omega</math>), any ordinal <math>\alpha</math> can be uniquely expressed in the form <math>\delta^{\beta_1}\gamma_1 + \ldots + \delta^{\beta_k}\gamma_k</math>, where <math>k</math> is a [[natural number]], <math>\gamma_1,\ldots,\gamma_k</math> are non-zero ordinals less than <math>\delta</math>, and <math>\beta_1 > \beta_2 > \cdots > \beta_k</math> are ordinal numbers (we allow <math>\beta_k=0</math>). This "base <math>\delta</math> representation" is an obvious generalization of the [[Ordinal arithmetic#Cantor normal form|Cantor normal form]] (which is the case <math>\delta=\omega</math>). Of course, it may quite well be that the expression is uninteresting, i.e., <math>\alpha = \delta^\alpha</math>, but in any other case the <math>\beta_i</math> must all be less than <math>\alpha</math>; it may also be the case that the expression is trivial (i.e., <math>\alpha<\delta</math>, in which case <math>k\leq 1</math> and <math>\gamma_1 = \alpha</math>).

If <math>\alpha</math> is an ordinal less than <math>\varepsilon_{\Omega+1}</math>, then its base <math>\Omega</math> representation has coefficients <math>\gamma_i<\Omega</math> (by definition) and exponents <math>\beta_i<\alpha</math> (because of the assumption <math>\alpha < \varepsilon_{\Omega+1}</math>): hence one can rewrite these exponents in base <math>\Omega</math> and repeat the operation until the process terminates (any decreasing sequence of ordinals is finite). We call the resulting expression the ''iterated base <math>\Omega</math> representation'' of <math>\alpha</math> and the various coefficients involved (including as exponents) the ''pieces'' of the representation (they are all <math><\Omega</math>), or, for short, the <math>\Omega</math>-pieces of <math>\alpha</math>.

Line 101:

The notations thus defined have the property that whenever they nest <math>\psi</math> functions, the arguments of the "inner" <math>\psi</math> function are always less than those of the "outer" one (this is a consequence of the fact that the <math>\Omega</math>-pieces of <math>\alpha</math>, where <math>\alpha</math> is the largest possible such that <math>\psi(\alpha)=\delta</math> for some <math>\varepsilon</math>-number <math>\delta</math>, are all less than <math>\delta</math>, as we have shown above). For example, <math>\psi(\psi(\Omega)+1)</math> does not occur as a notation: it is a well-defined expression (and it is equal to <math>\psi(\Omega) = \zeta_0</math> since <math>\psi</math> is constant between <math>\zeta_0</math> and <math>\Omega</math>), but it is not a notation produced by the inductive algorithm we have outlined.

Canonicalness can be checked recursively: an expression is canonical [[if and only if]] it is either the iterated Cantor normal form of an ordinal less than <math>\varepsilon_0</math>, or an iterated base <math>\delta</math> representation all of whose pieces are canonical, for some <math>\delta=\psi(\alpha)</math> where <math>\alpha</math> is itself written in iterated base <math>\Omega</math> representation all of whose pieces are canonical and less than <math>\delta</math>. The order is checked by lexicographic verification at all levels (keeping in mind that <math>\Omega</math> is greater than any expression obtained by <math>\psi</math>, and for canonical values the greater <math>\psi</math> always trumps the lesser or even arbitrary sums, products and exponentials of the lesser).

For example, <math>\psi(\Omega^{\omega+1}\,\psi(\Omega) + \psi(\Omega^\omega)^{\psi(\Omega^2)}42)^{\psi(1729)\,\omega}</math> is a canonical notation for an ordinal which is less than the Feferman–Schütte ordinal: it can be written using the Veblen functions as <math>\varphi_1(\varphi_{\omega+1}(\varphi_2(0)) + \varphi_\omega(0)^{\varphi_3(0)}42)^{\varphi_1(1729)\,\omega}</math>.

Line 236:

* <math>\psi_\Omega(\alpha)</math> is the smallest countable ordinal ρ such that <math>C^\Omega(\alpha, \rho) \cap \Omega= \rho</math>

<math>\psi_\Omega(\varepsilon_{\Omega+1})</math> is the Bachmann–Howard ordinal, the proof-theoretic ordinal of Kripke–Platek set theory with the [[axiom of infinity]] (KP).

=== Buchholz's ''ψ'' ===

Line 332:

* {{cite journal | last=Buchholz | first=Wilfried | title=A New System of Proof-Theoretic Ordinal Functions | journal=Annals of Pure and Applied Logic | volume=32 | year=1986 | pages=195&ndash;207 | doi=10.1016/0168-0072(86)90052-7 | url=https://epub.ub.uni-muenchen.de/3841/ | doi-access=free }}

* {{cite journal | last=Rathjen | first=Michael | title=Proof-theoretic analysis of KPM | journal=Archive for Mathematical Logic | volume=30 | year=1991 | pages=377&ndash;403 | doi=10.1007/BF01621475 | issue=5–6 | s2cid=9376863 }}

* {{cite journal | last=Rathjen | first=Michael | title=Proof theory of reflection | journal=Annals of Pure and Applied Logic | volume=68 | year=1994 | pages=181&ndash;224 | url=http://www.maths.leeds.ac.uk/~rathjen/ehab.pdf | doi=10.1016/0168-0072(94)90074-4 | issue=2 | archive-date=2020-10-21 | access-date=2008-05-10 | archive-url=https://web.archive.org/web/20201021105352/http://www1.maths.leeds.ac.uk/~rathjen/ehab.pdf | url-status=dead }}

* {{cite journal | last=Rathjen | first=Michael | title=Recent Advances in Ordinal Analysis: <math>\Pi^1_2</math>-CA and Related Systems | journal=The Bulletin of Symbolic Logic | volume=1 | year=1995 | pages=468&ndash;485 | url=https://www.math.ucla.edu/~asl/bsl/0104/0104-004.ps | doi=10.2307/421132 | jstor=421132 | issue=4 | s2cid=10648711 }}

* {{cite journal | last=Kahle | first=Reinhard | title=Mathematical proof theory in the light of ordinal analysis | journal=Synthese | volume=133 | year=2002 | pages=237&ndash;255 | doi=10.1023/A:1020892011851 | s2cid=45695465 }}

* {{cite journal | last=Rathjen | first=Michael | title=An ordinal analysis of stability | journal=Archive for Mathematical Logic | volume=44 | year=2005 | pages=1&ndash;62 | url=http://www.maths.leeds.ac.uk/~rathjen/NSTAB.ps | doi=10.1007/s00153-004-0226-2 | citeseerx=10.1.1.15.9786 | s2cid=2686302 | archive-date=2022-12-20 | access-date=2008-05-10 | archive-url=https://web.archive.org/web/20221220161823/http://www1.maths.leeds.ac.uk/~rathjen/NSTAB.ps | url-status=dead }}

* {{cite web | url=http://www.mathematik.uni-muenchen.de/~aehlig/EST/rathjen4.pdf | title=Proof Theory: Part III, Kripke–Platek Set Theory | accessdate=2008-04-17 | last=Rathjen | first=Michael | date=August 2005 | archive-url=https://web.archive.org/web/20070612112202/http://www.mathematik.uni-muenchen.de/~aehlig/EST/rathjen4.pdf | archive-date=2007-06-12 | url-status=dead }}(slides of a talk given at Fischbachau)