Is there a way, using set comprehension, to denote the closure of a set under a particular operation?
For example, if $\mathrm{succ}(n)$ denotes the successor operator $n \mapsto n \cup \{n\}$, then the set $\mathbb N$ of natural numbers can be described as the closure of the set $\{0\}$ under the operator $\mathrm{succ}(n)$. But how can this be written using set comprehension? Would it be something like this?
$$\mathbb N = \{0\} \cup \{\mathrm{succ}(n):n\in\mathbb N\}$$
Or would I have to define, say,
\begin{align*}
\mathbb N_0 &= \{0\}\\
\mathbb N_i &= \{\mathrm{succ}(n) : n\in \mathbb N_{i-1}\}\\
\mathbb N &= \bigcup_{i = 0}^\infty \mathbb N_i
\end{align*}
It seems odd using a union with indices to define the natural numbers though!
Best Answer
If you're just interested in defining $\mathbb{N}$, then the usual way to do it in ZF is via the axiom of infinity. This axiom guarantees the existence of at least one set which is inductive which means that it contains the empty set and all successors of its own elements. $\mathbb{N}$ (usually called $\omega$ in set theory) is then the intersection of all inductive sets, i.e. the smallest inductive set. (You need at least one inductive set in order for the intersection to be well-defined.)