# Is “theory of classes” “constructive” in NBG and ZFC? How to state theorems about “classes” involving $\exists!$?

The underlying philosophy of constructivism in mathematics is that in order to prove that something exists, we need to "find" or "construct" it.

In NBG (von Neumann–Bernays–Gödel axiomatic set theory) one can only quantify over sets, as in ZFC (where classes can also be informally treated specifying formulas, for example, instead of $\alpha \in \mathrm{Ord}$ we simply say that $\alpha$ satisfy the formula which asserts as set to be an ordinal).

However, what if we want, for example, to state a theorem that asserts an existence of a certain class? For example, take Transfinite Recursion:

Transfinite Recursion. Let $G\colon V \to V$ be a class function ($V$ being a class of all sets). Then there is a unique class function $F\colon \mathrm{Ord} \to V$ such that $$\forall \alpha \in \mathrm{Ord}, F(\alpha) = G(F\restriction_{\alpha}).$$

I've been thinking how can we state this theorem in the language of ZFC and NBG. In ZFC, a "class function" from a "class" define by a formula $\phi(x)$ to a class defined by a formula $\psi(y)$ is simply a formula $\upsilon(x,y)$ such that $\forall x, \phi(x) \Rightarrow \exists!y \in \psi(y), \upsilon(x,y)$. The problem is the same: we can't quantify neither over formulas in ZFC, nor over classes in NBG.

In transfinite recursion, we can simply circumvent the issue of not being able to write "for all class functions $G\colon V \to V$" is to treat is not as an theorem, but an infinitely many theorems, one for each different formula representing a class function.

However, we still can't simply state that some class or some class function "exists". But, apparently, we don't have to. The proof of the aforementioned theorem I know of involves the explicit construction of a class function $F\colon \mathrm{Ord} \to V$ by defining a formula.

So, to prove that some class (or a class function, which is still a class in NBG) exists, we have to explicitly construct it? So, in way, theory of classes is "constructive" in NBG (and in ZFC, even if there is no theory of classes per se)?

That is, instead of saying that there exists class function, we simply state a formula (I will not write it here, as it is long and requires auxiliary definitions) and prove that it does indeed defines a class function?

But if this is the case, what about uniqueness? To say that there are no other sets $y$ satisfying $\phi(y)$ rather than $x$ is precisely to say that $\forall y, \phi(y) \Rightarrow y = x$. But we can't even say $\forall y,$ if $y$ is a class function.

I understand many here will want a precise question (or questions) rather than a wall of text, so I'll sum my questions up:

$(1)$ Is giving an explicit construction of a class or a class function the only way of saying that it exists in NBG or ZFC?

$(2)$ If so, how do we say that there is no other class with that property?

P.S. This question is not only about proving something involving unquantifiable objects in a theory, but also about stating theorems about them.

First of all, you can quantify over classes in NBG: in NBG, unlike ZFC, variables can refer to classes, and you are free to quantify over these variables. So there is no difficulty at all formulating something like recursion over $Ord$ in NBG.
In ZFC, you are correct that since you can only refer to classes by writing down specific formulas, you can only prove that a class with certain properties "exists" by exhibiting a formula for it. As for uniqueness, it doesn't actually present any challenge you haven't already described how to handle. Just like you handled "for all $G:V\to V$" by a theorem schema, you can handle the universal quantifier in expressing uniqueness by a theorem schema. That is, for each pair of formulas $F$ and $F'$, you have a separate theorem saying that if $F$ and $F'$ both satisfy the condition then $F$ and $F'$ define the same class.
In certain specific examples, there may be ways to indirectly make quantified statements over classes with just a single sentence in ZFC. For instance, consider the statement "there exists a class which is a well-ordering of $V$". A priori, this cannot be expressed in ZFC without specifying a specific formula which you are using to well-order $V$. However, you can prove a theorem that says there exists a class which well-orders $V$ iff there exists a set $A$ such that $V=HOD[A]$. More precisely, assuming $V=HOD[A]$, you can write down a specific class which well-orders $V$, and you can prove a theorem schema saying that for any class $F$, if $F$ well-orders $V$, then there exists a set $A$ such that $V=HOD[A]$. So for practical purposes, you can use the statement "there exists a set $A$ such that $V=HOD[A]$" (which is a perfectly good sentence in the language of ZFC) as a proxy for the statement "there exists a class which is a well-ordering of $V$".
• What is more, I'm not sure how would we make a "theorem schema" within a "theorem schema". Maybe, we can make an additional theorem schema saying that given three formulas $P(x,y), R(x,y)$ and $T(x,y)$ such that $\forall x \exists! y, P(x,y)$... – Jxt921 Aug 3 '17 at 4:05
• As for a "theorem schema within a theorem schema", you have the right idea. For every triple (or whatever $n$-tuple you need) of formulas, you have a separate theorem. This is no more difficult to do with several formulas at once than it is with a single formula. – Eric Wofsey Aug 3 '17 at 4:11