How does one construct $\omega + \omega$ in ZFC?

Question

I can't figure out what axioms allow me to construct it. Most of the answers I've encountered say to define $f(x,y) := y = \omega + x$ and use Replacement, but I don't see how that would work. $+$ requires a recursive definition, and each instance of Replacement will use a fixed wff, so I can't encode recursion that way.

I'm looking for a specific sequence of axioms in ZFC I can apply which will prove the existence of the set $\omega + \omega$.

We have ω by using Specification on Infinity with a class function that says it has all sets which are in all inductive functions. We have $\omega + k$ for some arbitrary $k$ by taking successor, $x \cup \{x\}$, with itself $k$ times. Can't figure out how to get beyond that.

Answer 1

You've mentioned that we can construct $\omega + k$ as a successor ordinal, which is true for some natural number $k$, but this approach doesn't work for $\omega + \omega$. However, this is still useful, as we can think of $\omega + \omega$ as exactly the least such ordinal which is not $\omega$ or a successor ordinal.

Using first order logic, we can describe the necessary conditions like 'being a successor' to construct $\omega + \omega$.

Answer 2

I talked to a buddy of mine who managed to get a formula figured out. It's a doozy. Can define a function x -> $\omega + x$ in the following way.

Let <x,y> be ordered pair {{x}, {x,y}}, g(x) denote the unique value y such that <x,y> $\in$ a set function g, Im g all k such that <x, k> $\in g$

f(x,y,A) := (g is a set function x -> y) $ \land (\omega = y - Im\ g)\ \land\ \forall m \in x(\forall v(v \in g(m) \iff (v \in \omega\ \lor\ \exists u \in m (v = g(u)))))$

Then, with domain $\mathbb{N}$, we use with with Replacement and should get $\omega + \omega$.

The actual sets g that the formula generates don't matter, but the first few are:

$F(0, \omega, \mathbb{N}) \to g = \{\}$

$F(1, \omega+1, \mathbb{N}) \to g = \{<0, \omega>\}$

$F(2, \omega+2, \mathbb{N}) \to g = \{<0, \omega>, <1, \omega + 1>\}$