CGV googology part 1: veblen function

Hello, this post will be introducing a small (and presumably the most successful) portion of the fascinating subject of combinatorial game value or surreal googology. This is the Veblen function $\varphi :\mathrm{On}\times \mathrm{No}\mapsto \mathrm{No}$, defined in two different ways by me and PlanetN9ne, and later shown to be equivalent (by me!).

Note, there is a veblen function $\varphi :\mathrm{No}\times \mathrm{No}\mapsto \mathrm{No}$ but it’s cursed. Most of this is due to the fact that $\varphi (\frac{1}{2})$ enumerates some fixed points of $x\mapsto {\omega }^x$ which are already values of $\varphi (1)$.

My definition

$\varphi (x,y)=\{0,r\varphi (x,y^L),\varphi (x^{\prime },\varphi (x,y{)}^L)|r\varphi (x,y^R),\varphi (x^{\prime },\varphi (x,y{)}^R)\}$, where $x^{\prime }$ ranges over ordinals less than $x$, $r$ ranges over all positive real numbers, and $y^L$ and $y^R$ range over left and right sets of $y$.

Planet’s definition

First, we need to discuss sign expansions. Look it up.

Secondly, we need to discuss a method that interpolates all “hypernormal” ordinal functions. A function f is hypernormal if it is normal and $\alpha <\beta$ implies $f(\alpha )+f(\beta )=f(\beta )$.

For any surreal $x$, let $s_1,s_2,\dots$ be the sign expansion of $x$. Then we can define the interpolated function $f$ by $f(x)={+}^{f(0)}{s}_1^{f(1)}{s}_2^{f(2)}\dots$. This agrees with $f$ on all ordinal values. Proof by induction: obviously true for 0, and $f(\alpha +1)$’s sign-expansion is just that of $f(\alpha$\) with $f(\alpha +1)$ pluses added. So it is the ordinal sum $f(\alpha )+f(\alpha +1)$ which is $f(\alpha +1)$ by hypernormality. The limit case follows from normality.

Planet’s veblen is obtained by interpolating the second argument of veblen in this manner. We use $\phi$ to denote it.

Proof of equivalence

The following properties hold of Planet’s veblen function:

1. $\phi (\alpha ,x)$ is increasing, because $\phi (\alpha )$ repeats every sign some number of times and adds some signs to the front, which clearly preserves comparison.
2. $\phi ({\alpha }^{\prime },\phi (\alpha ,x))=\phi (\alpha ,x)$, given ${\alpha }^{\prime }<\alpha$.. Proof: let the sign expansion of $x$ be $stu\dots$. Then that of $\phi (\alpha ,x)$ is ${+}^{\varphi (\alpha ,0)}{s}^{\varphi (\alpha ,1)}\dots$, and that of $\phi ({\alpha }^{\prime },\phi (\alpha ,x))$ is ${+}^{\varphi ({\alpha }^{\prime },0)}$${+}^{\varphi ({\alpha }^{\prime },1)+\dots +\text{up to but not including }\varphi ({\alpha }^{\prime },\varphi (\alpha ,1))}$$s^{\varphi ({\alpha }^{\prime },\varphi (\alpha ,1))+\dots +\text{up to but not including }\varphi ({\alpha }^{\prime },\varphi (\alpha ,2))}\dots$$={+}^{\varphi (\alpha ,0)}{s}^{\varphi (\alpha ,1)}\dots$.
3. $\phi (\alpha ,x)$ is simpler than $\phi (\alpha ,y)$ if $x$ is simpler than $y$, because it applies $\varphi (\alpha )$ to the birthday.
4. Every common fixed point of $\phi ({\alpha }^{\prime })$ for ${\alpha }^{\prime }<\alpha$ is of the form $\phi (\alpha ,x)$. Proof: let the fixed point be $y={+}^b{-}^c{+}^d{-}^e\dots$. (It has to start with a plus because every value is positive.) Then it’s easy to see (similarly to (2)) that $b,c,d,\dots$ are all fixed points of $\varphi ({\alpha }^{\prime })$, thus they are values of $\varphi (\alpha )$ making $y$ a values of $\phi (\alpha )$.
5. $\phi (\alpha ,x)$ is the simplest common fixed point of $\phi ({\alpha }^{\prime },y)$ between $\phi (\alpha ,x^L)$ and $\phi (\alpha ,x^R)$, which trivially follows from the previous.
6. $\phi (0,x)={\omega }^x$. Proof to be given at a later date.

But $\varphi$ is, by construction, the unique function satisfying (5) and (6). Thus, $\varphi =\phi$.