How do we define recursive class functions like $\alpha \mapsto V_\alpha$ and $\alpha \mapsto L_\alpha$ in the language of set theory?

Question

It is well-known that ZFC proves that everything is an element of $V$. Symbolically, $\forall x(x \in V).$ However, I can't figure out how to translate this into the language of ZFC. We know that $V$ is the union of the following stages:

1. $V_0 = \emptyset$
2. $V_{\alpha+1} = \mathcal{P}(V_\alpha)$
3. $V_\lambda = \bigcup_{\alpha<\lambda} V_\alpha$

Hence $x \in V$ can be defined as a shorthand for $\exists \alpha : \mathrm{Ordinal}(\alpha) \wedge x \in V_\alpha$. So all we have to do now is express $\alpha \mapsto V_\alpha$ in the language of set theory. But how?

Question. How do we define recursive class functions (like $\alpha \mapsto V_\alpha$) in the language of set theory?

Motivation. I want to express the axiom of constructibility (namely $V=L$) in the language of set theory.

Answer 1

For the purpose of $V=L$, $V$ has a dead-simple definition - $V$ is the class of all sets $V=\{x|x=x\}$. You could use the "hierarchy" definition $V=\bigcup_{\alpha\in{\sf ON}}V_\alpha$, but that's overkill. But we'll definitely need to do this for $L$, so here are the steps:

• Define an "acceptable function" to be some function on an ordinal that satisfies the recursion relation
• Define the class-function $\alpha\mapsto L_\alpha$ as the union of all acceptable functions

I'll assume that you've already defined ${\cal P}_L$ as a function in set theory (which is itself quite complicated, involving the satisfiability predicate and Godel codes and all that). Then:

$$L=\bigcup\{f:\exists x\in{\sf ON}(f:x\to V\wedge\forall y\in x\,f(y)=\\{\rm if}(y=\emptyset,\emptyset,{\rm if}(y={\small\bigcup}y,{\small\bigcup}f[y],{\cal P}_L(f({\small\bigcup}y)))))\}$$

Let's break this down a little. The end expression ${\rm if}(y=\emptyset,\emptyset,{\rm if}(y={\small\bigcup}y,{\small\bigcup}f[y],{\cal P}_L(f({\small\bigcup}y)))$ is a division into cases: If $y$ is the empty set, return the empty set; if $y$ is a limit ordinal, which is to say $y=\bigcup y$, then return the union of all previous $f(y)$'s, which is concisely expressed as $\bigcup f[y]$, where $f[y]$ is the image of the function $f$ under the set $y$. Otherwise $y$ is a successor, and the predecessor of $y$ is $\bigcup y$. Then ${\cal P}_L(f({\small\bigcup}y))$ gives us the $L$-powerset of the previous value.

This is all set equal to the value of $f(y)$, so we are specifying the values of $f$ in terms of all the previous values. The transfinite recursion theorem ensures that for a given domain ordinal $x$, there is a unique function satisfying all these properties, and for different domain ordinals, the functions are end-extensions of each other, so that the union of all such functions is a single well-defined function on ${\sf ON}$.

This defines the function $L:{\sf ON}\to V$ such that $L(\alpha)=L_\alpha$ according to the usual rules, that is: $L(\emptyset)=\emptyset$, $L(\operatorname{suc}\alpha)={\cal P}_L(L(\alpha))$, and $L(\delta)=\bigcup_{\beta<\alpha}L(\beta)$ when $\delta$ is a limit ordinal. It also helps to examine this definition and the theorems proving its correctness on Metamath. Then the class $L$ is defined as $\bigcup L[{\sf ON}]$, the union of the range of this function, and the axiom of constructibility could be phrased directly as $V=\bigcup L[{\sf ON}]$, or after some definition unpacking as

$$\forall x\,\exists y\in{\sf ON}\,x\in L(y).$$

If you replace ${\cal P}_L$ everywhere with ${\cal P}$, you get instead the function $\alpha\to V_\alpha$, and there is a nontrivial theorem depending essentially on the axiom of foundation that shows that the range of this function is $V$. (It appears you take the opposite stance in your post, where $V$ is defined to be this union and the nontrivial theorem says that every set is in $V$. Just so we're clear, I define $V$ to be the class builder I mentioned at the beginning.) In fact, $V=\bigcup_{\alpha\in{\sf ON}}V_\alpha$ is an equivalent of the axiom of foundation.

Answer 2

The idea is similar to the method of encoding recursive definition in $\sf PA$. We use recursion and the fact that we can "access" sequences of sets to say something "$F(\alpha)=X_\alpha$ if there is a sequence of sets of length $\alpha$, such that bla bla bla".

For example, in the case of the function $V(\alpha)=V_\alpha$ we can write the following statement:

$V(\alpha)=x$ if and only if there exists a sequence of sets of length $\alpha$, $\langle x_i\mid i\leq\alpha\rangle$ such that $x_0=\varnothing$, for every $i$, $x_{i+1}$ is the power set of $x_i$, and if $j$ is a limit ordinal then $x_j=\bigcup\{x_i\mid i<j\}$, and $x=x_\alpha$.

Note that all those can be written in the language of set theory. It is just a horrible pain in the lower lower back to do so.

Similarly, $L(\alpha)=x$ is even more complex since we don't just write $x_{i+1}$ is the power set of $x_i$, but rather the definable power set of $x_i$ over the language $\{\in\}$. This requires us to refer to another definition of truth predicates, formulas, logic, and so on and so forth.

But once you know that there is a formula $\psi(S,M,\ulcorner\varphi(x,u)\urcorner,p,A)$ whose content is "$S$ is a first-order language, and $M$ is an interpretation for $S$, and $\ulcorner\varphi(x,p)\urcorner$ is a formula with free variables $x$ and $u$ (parameters), and $A$ is the set $\{x\in M\mid M\models\varphi[x,p]\}$", then it's as easy as before.

Note that I didn't even bother specifying that these things are only defined for ordinals. Of course, if $a$ is not an ordinal, we just define $V(a)=\varnothing$ or something, which is yet another [ultimately unimportant] complication to the description of the function $\alpha\mapsto V_\alpha$.