# Does iterating any definable in ZFC functional relation give a $\mathbb N$-indexed family of sets?

Consider an extension of ZFC (the first-order theory with signature $\in$ and the usual axioms) by a constant $x$, and a binary relation $N$ that is functional, i.e., we have the additional axiom

• $\forall x\exists!y\,N(x,y)$

and a constant $x_0$.

My question is whether there is a proof from the axioms that there exists a set $S$ and a set-function $f\colon\mathbb N\to S$ so that $n\in\mathbb N\rightarrow N(f(n),f(n+1))$ and $f(0)=x_0$?

There is also an equivalent way of phrasing the question since the existence of such an $f$ implies that the two-variable formula $\phi(n,x)$ given by $\phi(n,x)\equiv f(n)=x$ satisfies:

1. $\exists! x\,\phi(0,x)$
2. $\phi(0,x_0)$
3. $\forall n\left(n\in\mathbb N\rightarrow \forall y\left(\left(\exists x\left(\phi(n,x)\wedge N(x,y)\right)\right)\leftrightarrow\phi(n+1,y)\right)\right)$

and conversely, given such a formula $\phi$, since ZFC implies the induction principle of $\mathbb N$, we can derive from those properties that $\phi$ is functional ($\forall n\left(n\in\mathbb N\rightarrow\exists!x\,\phi(n,x)\right)$), by the axiom schema of replacement we obtain the existence of our desired set $S$ and the function $f$.

Hence my question is equivalent to asking whether there exists such a formula in the language of this extension.

My question is ill-posed and its answer depends on whether I intend on extending the axiom schemes of replacement and comprehension to formulas involving the functional $N$.

If the axiom schemes are not extended, then the answer is clearly no as we can see by taking a countable model of ZFC, $x_0=$the zeroeth element uneder an enumeration, and $N$ the increment of that enumeration (which is what the accepted answer says).

If the axiom schemes are extended, then the answer is yes, and the formula $\phi$ given by the the usual argument establishing that transfinite recursion works.

Specifically, (and with shorthands) $\phi(n+1,x)$ is given by "$x=g(n+1)$ where $g$ is any function $g\colon\{0,\dots,n+1\}\to T$ to a set $T$ such that $g(0)=x_0$ and $g(n+1)=T(g(n))$".

• Given a model $V_\alpha$ of ZFC with $cf(\alpha) = \omega$ and $y_0,...,y_n,...$ a co-final sequence in $\alpha$, let $x_0 = y_0$ and $N(y_n, y_{n+1})$. Then if there were such an $f$ in $V_\alpha$ the union of it's range would be $\alpha$ and would be in $V_\alpha$ which is impossible.
– user104955
Commented Jan 8, 2014 at 7:34
• If N is definable, you can inductively construct S. This is a simple application of replacement. Commented Jan 8, 2014 at 8:38

1. The axiom scheme $$(\forall x)(\exists y)\phi(x,y) \to (\forall x)(\exists \langle z_i : i \in \omega\rangle)(\forall i \in \omega)[z_0 = x \land \phi(z_i,z_{i+1})]$$ is a form of the principle of dependent choice that is provable in ZFC.
2. If you extend the axiom schemes (comprehension and replacement) in ZFC to the new larger class of formulas (including $N$), then dependent choice for this larger language will also be provable. That will give an affirmative answer to the question. Similarly, if we make a extension by definitions that defines $N$, then dependent choice for the larger class of formulas will be provable.
3. If you extend the language but don't extend the axiom schemes to match, there is no reason to suspect you can prove things about $N$. For example, if $A$ is infinite, you can't even form $\{N(x) : x \in A\}$.
• Of course you don't need choice when you know $(\forall x)(\exists ! y)\phi(x,y)$, for the standard reasons. Commented Jan 8, 2014 at 13:06