Can we formulate V=L inside ZF?

Question

Is V=L a metatheory statement, or can this statement be formulated inside ZF?

Answer 1

Although not obvious, it can indeed be formulated in the language of set theory (incidentally, the same is true of $V=HOD$ - this requires a trick, since the obvious approach seems to require a definition of truth in $V$). The details are covered carefully in Kunen's text.

EDIT: As per Eric Wofsey's comment, expressing "$V=L$" in the language of set theory amounts to defining $L$ in the language of set theory (since then we just say "all sets are in $L$"), and the latter is necessary to even metatheoretically define $L^M$ for illfounded models $M$ (how do you perform a recursive definition along an ill-founded ordering, unless you're doing it inside some smaller model that things the ordering is well-founded?). So the sequence of ideas here is: we first define $L^N$ for well-founded $N$ in the metatheory, then show how to define $L^M$ for general (= possibly ill-founded) models, and this in fact subsumes the task of expressing "$V=L$" in the language of set theory.

One approach is straightforward:

• First, show that the formula "$x$ is a definable subset of $y$" (where $x\subseteq y$, $y$ is a transitive set, and we're viewing $y$ as an $\{\in\}$-structure) is expressible in the language of set theory. The key point is that since $y$ is a set, we can talk about Skolem functions over $y$; this doesn't work for trying to define definability with respect to $V$.

• With that in hand, we can now define an $L$-sequence to be a sequence indexed by some ordinal whose $0$th term is $\emptyset$, whose limit terms are given by unions, and whose successor terms are given by definable powersets. "$V=L$" is then shorthand for "Every set is a member of some term of some $L$-sequence."

There is also - surprisingly, in my opinion - a purely combinatorial approach discovered by Godel: that $L$ is the closure of the ordinals under a small list of basic operations. It should be clear that $L$ contains the closure of the ordinals under these operations, since they're definable; the converse is nontrivial but true. So this gives another way to express "$V=L$" in the language of set theory.

Of course, ultimately the metatheory rears its head when we try to argue that the formalizations of "$V=L$" in the language of set theory actually match the metatheoretic statement "$V=L$," but it's pretty clear they do. In particular, a reasonable metatheory can prove that a well-founded $M\models ZFC$ satisfies $V=L$ iff $M=L^M$, where $L^M$ is defined in the metatheory as usual.