Ist „Klassentheorie“ in NBG und ZFC „konstruktiv“? Wie kann man Sätze über „Klassen“ aufstellen, die ∃!∃!\exists! beinhalten?

Die zugrunde liegende Philosophie des Konstruktivismus in der Mathematik ist, dass wir, um zu beweisen, dass etwas existiert, es „finden“ oder „konstruieren“ müssen.

In NBG (von Neumann-Bernays-Gödel axiomatische Mengenlehre) kann man nur über Mengen quantifizieren, wie in ZFC (wo Klassen auch informell behandelt werden können, indem man beispielsweise Formeln angibt, anstatt$\alpha \in \mathrm{Ord}$das sagen wir einfach$\alpha$die Formel erfüllen, die behauptet, eine Ordinalzahl zu sein).

Was aber, wenn wir zum Beispiel einen Satz aufstellen wollen, der die Existenz einer bestimmten Klasse behauptet? Nehmen Sie zum Beispiel Transfinite Recursion :

Transfinite Rekursion . Lassen$G\colon V \to V$sei eine Klassenfunktion ($V$eine Klasse aller Mengen sein). Dann gibt es eine eindeutige Klassenfunktion$F\colon \mathrm{Ord} \to V$so dass

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

Ich habe darüber nachgedacht, wie wir diesen Satz in der Sprache von ZFC und NBG formulieren können. In ZFC lässt sich eine „Klassenfunktion“ aus einer „Klasse“ durch eine Formel definieren$\phi(x)$zu einer durch eine Formel definierten Klasse$\psi(y)$ist einfach eine Formel$\upsilon(x,y)$so dass$\forall x, \phi(x) \Rightarrow \exists!y \in \psi(y), \upsilon(x,y)$. Das Problem ist dasselbe: Wir können weder über Formeln in ZFC noch über Klassen in NBG quantifizieren.

Bei der transfiniten Rekursion können wir einfach das Problem umgehen, dass wir nicht "für alle Klassenfunktionen schreiben können$G\colon V \to V$„ ist nicht als ein Theorem zu behandeln, sondern als unendlich viele Theoreme, eine für jede verschiedene Formel, die eine Klassenfunktion darstellt.

Wir können jedoch immer noch nicht einfach sagen, dass eine Klasse oder eine Klassenfunktion "existiert". Aber anscheinend müssen wir das nicht. Der mir bekannte Beweis des vorgenannten Theorems beinhaltet die explizite Konstruktion einer Klassenfunktion$F\colon \mathrm{Ord} \to V$durch Definition einer Formel.

Um also zu beweisen, dass eine Klasse (oder eine Klassenfunktion, die in NBG immer noch eine Klasse ist) existiert, müssen wir sie explizit konstruieren? Also ist die Klassentheorie in gewisser Weise "konstruktiv" in NBG (und in ZFC, auch wenn es keine Klassentheorie per se gibt)?

Das heißt, anstatt zu sagen, dass es eine Klassenfunktion gibt, geben wir einfach eine Formel an (ich werde sie hier nicht schreiben, da sie lang ist und Hilfsdefinitionen erfordert) und beweisen, dass sie tatsächlich eine Klassenfunktion definiert?

Aber wenn dies der Fall ist, was ist mit der Einzigartigkeit? Zu sagen, dass es keine anderen Sets gibt$y$befriedigend$\phi(y)$statt$x$ist genau das zu sagen$\forall y, \phi(y) \Rightarrow y = x$. Aber wir können es nicht einmal sagen$\forall y,$Wenn$y$ist eine Klassenfunktion.

Ich verstehe, dass viele hier eher eine präzise Frage (oder Fragen) als eine Textwand wollen, also fasse ich meine Fragen zusammen:

$(1)$Ist die Angabe einer expliziten Konstruktion einer Klasse oder einer Klassenfunktion die einzige Möglichkeit zu sagen, dass sie in NBG oder ZFC existiert?

$(2)$Wenn ja, wie können wir sagen, dass es keine andere Klasse mit dieser Eigenschaft gibt?

PS Bei dieser Frage geht es nicht nur darum, etwas zu beweisen, das nicht quantifizierbare Objekte in einer Theorie beinhaltet, sondern auch darum, Theoreme darüber aufzustellen.