¿Es la "teoría de clases" "constructiva" en NBG y ZFC? ¿Cómo enunciar teoremas sobre "clases" que involucran ∃!∃!\exists!?

La filosofía subyacente del constructivismo en matemáticas es que para probar que algo existe, necesitamos "encontrarlo" o "construirlo".

En NBG (teoría axiomática de conjuntos de von Neumann-Bernays-Gödel) solo se puede cuantificar sobre conjuntos, como en ZFC (donde las clases también se pueden tratar informalmente especificando fórmulas, por ejemplo, en lugar de$\alpha \in \mathrm{Ord}$simplemente decimos que$\alpha$satisfacer la fórmula que afirma que un conjunto es un ordinal).

Sin embargo, ¿qué pasa si queremos, por ejemplo, enunciar un teorema que afirme la existencia de cierta clase? Por ejemplo, tome Transfinite Recursion :

Recursión transfinita . Dejar$G\colon V \to V$ser una función de clase ($V$siendo una clase de todos los conjuntos). Entonces hay una función de clase única$F\colon \mathrm{Ord} \to V$tal que

$$\forall \alpha \in \mathrm{Ord}, F(\alpha) = G(F\restriction_{\alpha}).$$

He estado pensando cómo podemos enunciar este teorema en el lenguaje de ZFC y NBG. En ZFC, una "función de clase" de una "clase" definida por una fórmula$\phi(x)$a una clase definida por una fórmula$\psi(y)$es simplemente una fórmula$\upsilon(x,y)$tal que$\forall x, \phi(x) \Rightarrow \exists!y \in \psi(y), \upsilon(x,y)$. El problema es el mismo: no podemos cuantificar ni sobre fórmulas en ZFC, ni sobre clases en NBG.

En la recursividad transfinita, podemos simplemente eludir el problema de no poder escribir "para todas las funciones de clase$G\colon V \to V$" es tratar no como un teorema, sino como un número infinito de teoremas, uno para cada fórmula diferente que representa una función de clase.

Sin embargo, todavía no podemos afirmar simplemente que alguna clase o alguna función de clase "existe". Pero, aparentemente, no tenemos que hacerlo. La demostración del teorema antes mencionado que conozco implica la construcción explícita de una función de clase$F\colon \mathrm{Ord} \to V$definiendo una fórmula.

Entonces, para probar que existe alguna clase (o una función de clase, que sigue siendo una clase en NBG), ¿tenemos que construirla explícitamente? Entonces, en cierto modo, ¿la teoría de clases es "constructiva" en NBG (y en ZFC, incluso si no hay una teoría de clases per se)?

Es decir, en lugar de decir que existe una función de clase, simplemente establecemos una fórmula (no la escribiré aquí, ya que es larga y requiere definiciones auxiliares) y demostramos que sí define una función de clase.

Pero si este es el caso, ¿qué pasa con la singularidad? Decir que no hay otros conjuntos$y$satisfactorio$\phi(y)$en vez de$x$es precisamente decir que$\forall y, \phi(y) \Rightarrow y = x$. Pero ni siquiera podemos decir$\forall y,$si$y$es una función de clase.

Entiendo que muchos aquí querrán una pregunta precisa (o preguntas) en lugar de un muro de texto, así que resumiré mis preguntas:

$(1)$¿Dar una construcción explícita de una clase o una función de clase es la única forma de decir que existe en NBG o ZFC?

$(2)$Si es así, ¿cómo decimos que no hay otra clase con esa propiedad?

PS Esta pregunta no se trata solo de probar algo que involucre objetos no cuantificables en una teoría, sino también de establecer teoremas sobre ellos.