# Formula defining the first transfinite ordinal $\omega$

Just as an exercise in formula manipulation, I tried to find the simplest formula $\phi(x)$ with one free variable $x$ in the language of ZFC that defines the first transfinite ordinal $\omega$ (i.e. $\phi(x) \leftrightarrow x=\omega$). Here is my attempt (operator precedence follows the Wikipedia): \begin{align}\phi(x):=\exists a (a \in x) \land \forall a \forall b \forall c ((a \in x \lor a = x) \to (c \in b \to (b \in a \to c \in a))) \land \\ \forall a (a \in x \to (\exists b (a \in b \land b \in x) \land (\exists b (b \in a) \to \exists b (b \in a \land \neg \exists c (b \in c \land c \in a)))))\end{align} It means that $x$ is non-empty ordinal (transitive set with transitive elements) that is not a successor ordinal, but each its non-empty element is a successor ordinal.

Is this formula correct? Can anybody suggest further simplification?

-
Is the second conjunct supposed to be $$\forall a\forall b\forall c\bigg((a\in x\lor a=x)\to \big((c\in b\land b\in a)\to c\in a\big)\bigg)\;?$$ Please don’t rely entirely on operator precedence; use parentheses to make the thing more readable. –  Brian M. Scott Dec 5 '11 at 3:12
Perhaps you can add a few words explaining what it is you are trying to describe with the formulas? That might make checking it a bit easier. Also, is this simpler than writing out that $\omega$ is the smallest inductive set? –  Arturo Magidin Dec 5 '11 at 3:13
It appears that you’re trying to express: $x$ is non-empty and hereditarily transitive, and $\forall a\in x (a$ has a (not necessarily immediate) successor in $x$, and if $a$ is non-empty, it has an immediate predecessor$)$. Is that correct? –  Brian M. Scott Dec 5 '11 at 3:30
@BrianM.Scott: Yes, that is correct. –  Vladimir Reshetnikov Dec 5 '11 at 3:40

Recall that $\omega$ is an inductive set. It is the minimal inductive set.
\begin{align*} \varphi(x):=\Bigg(\varnothing\in x&\land\forall w\Big(w\in x\rightarrow w\cup\{w\}\in x\Big)\Bigg)\\ &\land\forall y\Bigg(\bigg(\varnothing\in y\land\forall w\Big(w\in y\rightarrow w\cup\{w\}\in y\Big)\bigg)\rightarrow\forall w\Big(w\in x\rightarrow w\in y\Big)\Bigg) \end{align*}
If you'd wish to avoid $\varnothing$ or $w\cup\{w\}$ they both can be replaced. It would make the formula considerably longer though. These two are defined as:
1. $x = \varnothing\iff\forall y(y\in x\rightarrow y\in y)$
2. $x=w\cup\{w\} \iff \forall z\Big((z\in w\lor z=w)\Leftrightarrow z\in x\Big)$