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.

  • $\begingroup$ @GME: $V_\alpha$ and $V_y$ are not in the language of set theory, there is only one relation symbol in the language, namely $\in$. For the recursive definitions, the OP should refer to transfinite recursion, which builds a functional formula doing the job. $\endgroup$ – zarathustra May 21 '14 at 12:42
  • $\begingroup$ I don't know the standard answer, but I imagine the schema of replacement plays a key role in defining $\alpha\mapsto V_\alpha$. Once you've proven the codomain for any fixed $\alpha$ exists, then the recursive definition works just fine. $\endgroup$ – Dustan Levenstein May 21 '14 at 12:43
  • $\begingroup$ @FPE I know. I assumed the OP knew about the recursive def given their 1,2, and 3 and was asking a further question. But then I realised they were really just asking how to do transfinite recursion (which is why I deleted my comment). $\endgroup$ – GME May 21 '14 at 13:31

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.

  • $\begingroup$ Thanks for the comprehensive answer. I'll study it more closely when time permits. $\endgroup$ – goblin May 21 '14 at 13:31
  • $\begingroup$ @user18921 Lol, apologies if it was too dense. You happened to hit on exactly my specialty :) I'm actually working on defining $V=L$ in Metamath at the moment. $\endgroup$ – Mario Carneiro May 21 '14 at 13:33
  • $\begingroup$ Cool! $\;\!\;\!$ $\endgroup$ – goblin May 21 '14 at 13:34

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$.

  • $\begingroup$ I hope my answer hasn't aggravated your back pain! $\endgroup$ – Mario Carneiro May 21 '14 at 20:37
  • $\begingroup$ What back pain? $\endgroup$ – Asaf Karagila May 21 '14 at 20:39
  • $\begingroup$ "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." $\endgroup$ – Mario Carneiro May 22 '14 at 1:29
  • $\begingroup$ If anything your lower-lower back should ache, not mine. $\endgroup$ – Asaf Karagila May 22 '14 at 6:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.