A bit of reverse math fun: how to ensure the existence of the ordinal $\omega^\omega$?

Question

Lately I was having some fun with axiomatizing the ordinals. This isn't a research project or anything, just a casual little side task to keep myself busy during the winter holidays.

I started out with the basic axioms to guarantee a linear order:

1. $\forall_x \neg x < x$
2. $\forall_x \forall_y \neg [x <y \lor y<x] \implies x=y$
3. $\forall_{x} \forall_{y} \forall_{z} [x<y \land y<z] \implies x<z$

And the following axiom scheme to guarantee a well-order:

4. $[\exists_x \phi(x)] \implies \exists_y \phi(y) \land \forall_{z: z<y} \neg \phi(z)$

Then I decided to try adding specific axioms ensuring the existence of certain numbers.

Ensuring the existence of $0$ is easy enough: you just need to assume that there is at least one ordinal. You don't neccessarily have to assume that it's the minimal ordinal to prove that there must be one. From now on, every axiom will depend on the existence of at least one ordinal.

Similarly, ensuring the existence of ordinals up to (but not including) $n$ simply requires assuming that there are at least $n$ distinct ordinals.

To ensure the existence of every finite ordinal, you simply have to add the axiom:

$$A_\omega : \forall_x \exists_y x<y$$

To talk about higher ordinals, it is convenient to first define the following predicates:

$$I^1(x) \equiv \top$$

$$I^{n+1}(x) \equiv \forall_{y: y<x} \exists_{z:y<z} I^{n}(z) \land z<x$$

It turns out that to ensure the existence of ordinals up to (but seemingly not including) $\omega^{n}$, it is sufficient to assume:

$$A_{\omega^n} : \forall_x \exists_{y:x<y} I^n(y)$$

To ensure that every number up to $\omega^\omega$ exists, it is sufficient to assume all the axioms $A_{\omega^1}, A_{\omega^2}, A_{\omega^3}, \cdots,A_{\omega^n},\cdots$.

I tried to achieve the same result with a single axiom, but my imagination failed me. I also can't seem to figure out how to ensure that $\omega^\omega$ and higher numbers must exist. Any tips on how to move forward would be much appreciated!

Answer 1

Unfortunately it might not be possible using a single axiom. If we consider the structure $(\textrm{Ord},<)$, only the ordinals $<\omega^\omega$ are first-order definable. So there isn't a first-order predicate $\phi$ in this language where $\omega^\omega$ is the least $\alpha$ such that $(\textrm{Ord},<)\vDash\phi(\alpha)$ (otherwise we could define $\omega^\omega$ as "the unique $\beta$ satisfying $\chi(\beta)\equiv\phi(\beta)\land\forall\gamma(\gamma<\beta\implies\lnot\phi(\gamma))$".)

---

What can we do?

• We can formulate "the successor of each ordinal exists": $\forall\alpha\;\exists\sigma\;\forall\xi\;(\alpha<\xi\implies\sigma\le\xi)$

• Along with this we can formulate the successor relation. We don't use the usual set-theoretic graph formulation since ordered pairs aren't in the domain of discourse, but we can construct a formula $\sigma(\alpha,\beta)$ meaning "$\beta$ is the successor of $\alpha$": $$\sigma(\alpha,\beta)\;\equiv\;\forall\xi\;(\alpha<\xi\implies\beta\le\xi)$$

• In a similar way, the addition relation is first-order definable. This construction is apparently much more complex, it appears on page 6 of Itay Neeman's "Monadic Definability of Ordinals".