Defining the constructible universe without model theory

Question

The constructible powerset is defined in Wikipedia as:

$$\operatorname{Def}(X) := \Bigl\{ \{ y \in X \mid (X,\in) \models \Phi(y,z_1,\ldots,z_n) \} \Big| \Phi \text{ is a wff and } z_{1},\ldots,z_{n} \in X \Bigr\}.$$

My question is whether this operator can be defined without the "models" notion being used here, only basic set operations. For comparison, consider the finite axiomatization of NBG. In the usual axiomatization we have the "single" axioms: extensionality, pairing, union, powerset, infinity, and limitation of size; plus one axiom schema for comprehension. It was later shown that this axiom schema can be replaced by some eight or so "Godel operators", each of which performs some simple set theoretic operation like $\{(b,(a,c))\mid(a,(b,c))\in R\}$, and together these operations can build anything that the original comprehension schema could produce.

Answer 1

I think that, in his book on the consistency of the continuum hypothesis (not the brief paper in the Proceedings of the National Academy but the book), Gödel uses what are now called the Gödel operations to define the constructible universe. I think Shoenfield's book "Mathematical Logic" uses the same approach. So the answer to the title of your question is yes. The body of your question asks for something more difficult, not just getting $L$ but getting the individual stages of the constructible hierarchy. That can undoubtedly be done by similar methods, but I don't recall ever seeing it worked out. It would be tedious work, and I suspect nobody cared about it enough to do the work.

Answer 2

Here is a more or less direct translation of the satisfaction predicate to class-forming rules. It is sufficient to consider the base rules $x=y,\ x\in y$ and the wff operations $\lnot\phi,\ \phi\land\psi,\ \exists x\phi$. In order to handle parameters, we will actually define the set

$$\DeclareMathOperator{\defn}{\operatorname{Def}_{\Bbb N}(X)}\defn=\Big\{\{\vec y\in X^{\Bbb N}\mid (X,\in)\models\Phi(\vec y,\vec z)\}\Big|\,n\in\Bbb N,\Phi\mbox{ is a wff and } \vec z\in X^n\Big\},$$

where the sets are collections of sequences on $\Bbb N$, and the wff $\Phi$ has the first $n$ variables (or some finite subset) set to the $z_i$. From this we can pick out the one-parameter formulas as $$\operatorname{Def}(X)=\{x\in{\cal P}(X)\mid\{\vec y\in X^{\Bbb N}\mid y_1\in x\}\in\defn\}.$$

• For equality, we demand $\emptyset\in\defn$ and $n\in\Bbb N,y\in X\to\{x\in X^{\Bbb N}\mid x_n=y\}\in\defn$.
• Similarly for elementhood, we demand $i,j\in\Bbb N\to\{x\in X^{\Bbb N}\mid x_i\in x_j\}\in\defn$. Since we can write $x_i\in y\leftrightarrow \exists x_j(x_j=y\land x_i\in x_j)$ and $y\in x_i\leftrightarrow \exists x_j(x_j=y\land x_j\in x_i)$, it is not necessary to supply these sets, and similarly for $x_i=x_j\leftrightarrow \forall x_k(x_k\in x_i\leftrightarrow x_k\in x_j)$.
• Negation yields complementation, which is to say $A\in\defn\to X^{\Bbb N}\setminus A\in\defn$.
• Conjunction yields intersection, so $A,B\in\defn\to A\cap B\in\defn$.
• The existence quantifier is interpreted as \begin{align} \{x\in X^{\Bbb N}\mid (X,\in)\models \exists x_i,\phi\}&=\{x\in X^{\Bbb N}\mid \exists y\in X,(X,\in)\models \phi[x_i\to y]\}\end{align} and by induction we are assuming that the latter class abstraction is a member of $\defn$, so this yields the rule $n\in\Bbb N,A\in\defn\to\{x\in X^{\Bbb N}\mid \exists y\in X,x[x_i\to y]\in A\}\in\defn$ (where $x[x_i\to y]$ is the sequence on $\Bbb N$ defined by $x[x_i\to y]_i=y$ and $x[x_i\to y]_j=x_j$ for $j\ne i$.

The operation $\defn$ is thus defined as the smallest class which satisfies all these closures. Explicitly:

\begin{align}\defn&=\bigcap\Big\{D\mbox{ algebra on }X^{\Bbb N}\mid\\ &\land \forall i,j\in\Bbb N,\{x\in X^{\Bbb N}\mid x_i\in x_j\}\in D\\ &\land \forall n\in\Bbb N,\forall y\in X,\{x\in X^{\Bbb N}\mid x_n=y\}\in D\\ &\land \forall n\in\Bbb N,\forall A\in D,\{x\in X^{\Bbb N}\mid \exists y\in X,x[x_i\to y]\in A\}\in D\Big\}\end{align}

Since ${\cal P}(X^{\Bbb N})$ clearly satisfies all these conditions, the intersection is well-defined.

Answer 3

On a related note: Proposition 1.3 of http://library.msri.org/books/Book39/files/marker.pdf shows that the strategy for "defining definability" (as Kunen calls it in his Set Theory text (1st ed)) works for arbitrary structures. A proof of the proposition is in Marker's Model Theory text (http://www.amazon.com/Model-Theory-Introduction-Graduate-Mathematics/dp/0387987606).