Ordinal collapsing functions appear in proof theory, and they are used to name large countable ordinals by using uncountable ordinals. Previously I posted a question about why $\psi(\alpha)$ is sometimes called a Mostowski collapse. However there seems to be an even more common description whose details appear less clear than the Mostowski collapse connection.
An ordinal collapsing function (OCF) is often defined as an ordinal $\psi(\alpha)$ satisfying some kind of "minimum gap" condition with respect to closures $C(\alpha)$ of a "simple" set of ordinals (often including the first uncountable ordinal $\Omega$) under several operations. For concreteness here are three examples:
- In this$^1$ set of course notes, Arai introduces an OCF $\psi$ for analysis of a fragment of ZFC. By induction on $\alpha$, $C(\alpha,\beta)$ is defined as the closure of $\{0,\Omega\}\cup\beta$ under ordinal addition, the Veblen function, and $\psi$ itself restricted to ordinals less than $\alpha$ (closure definition.) Then $\psi\alpha$ is simultaneously defined as the least $\beta<\Omega$ where $C(\alpha,\beta)\cap\Omega\subseteq\beta$ ("minimum gap in $C$" condition.)
- In $^2$, Wilken introduces functions $\vartheta^n_m(\alpha)$ for analyzing an system of elementary substructurehood introduced by Carlson. By induction on $\alpha$, $C^n_m(\alpha,\beta)$ is defined as the closure of $\Omega_m\cup\beta$ under ordinal addition, and two different restrictions of $\vartheta$ itself. $\vartheta^n_m(\alpha)$ is defined as the least $\beta<\Omega_{m+1}$ where $C^n_m(\alpha,\beta)\cap\Omega_{m+1}\subseteq\beta$ ("minimum gap in $C$" condition) and $\alpha\in C^n_m(\alpha,\beta)$.
- In $^3$, Pohlers introduces an OCF $\psi$ for analysis of a formal theory for inductive definitions. The sets $B(\alpha)$ are defined the same way as Arai's set $C(\alpha,1)$, but $\psi(\alpha)$ is defined as the least ordinal not in $B(\alpha)$ (an even more literal "minimum gap in $B$".)
However each of the above sources describe the $C$-sets as Skolem hulls! Arai explicitly refers to $C(\alpha,\beta)$ as "the Skolem hull of $\{0,\Omega\}\cup\beta$ under the functions $+$, $\varphi$ and $\psi\vert\alpha$", Schutte says something similar. Wilken characterizes many previous OCFs as Skolem-hull-based:
The general principle used to define these notations can be understood as a form of iterated Skolem hulling process (see Pohlers, [7]). We therefore refer to the notation systems of classical type as notations derived from Skolem hull operators ... The origins of this type of Skolem hull based notations go back to a modification of the Aczel-Feferman functions and the work of Bridge (see [1]) due to Schütte and Buchholz (see [2] and [3])".
Pohlers's explanation$^3$ is that "the ordinals in $B(\Omega^\Gamma)$ ... are all definable from $0$ and $\Omega$ by the functions $+$, $\varphi$, and $\phi$. For every ordinal $\alpha$ in $B(\Omega^\Gamma)$ we therefore have a Skolem term $\underline\alpha$, built up from the symbols $0$, $\Omega$, $+$, $\varphi$ and $\psi$, denoting the ordinal $\alpha$." However this makes the roles of $+$, $\varphi$, $\psi$ sound more like function symbols used to construct terms, under which interpretation each $\alpha\in B(\Omega^\Gamma)$ has an associated variable-free term. On the other hand, when Skolem functions are utilized, Skolem functions for formulae with quantifiers is common, e.g. when $\forall x\exists y\phi(x,y)$ is Skolemized to $\forall x\phi(x,h(x))$. I am not sure either if there is any language custom-tailored to the construction of $C$ such that $\psi$ is a usual Skolem function for some formulae of that language. If they don't appear to be used in Skolemizing formulae, is there a connection which allows us to call $+$, $\varphi$, $\psi$ Skolem functions? If not, are the $C$-sets able to be called Skolem hulls?
$^1$: T. Arai, "Introduction to ordinal analyses" (2003, researchmap page).
$^2$: G. Wilken, "Ordinal arithmetic based on Skolem hulling". Annals of Pure and Applied Logic v. 145, 2007, ScienceDirect page.
$^3$: W. Pohlers, "Proof theory and ordinal analysis" (Arch. Math. Logic, v. 30, 1991).
