Kann die Tatsache, dass NBG ohne Wahl eine konservative Erweiterung von ZF ist, in der Peano-Arithmetik bewiesen werden?

Betrachten Sie NBG ohne Wahl. Bezeichnen Sie diese Theorie mit NBG'. Es ist ziemlich einfach, wenn man ein bisschen Modelltheorie kennt, um zu zeigen, dass diese Theorie eine konservative Erweiterung von ZF ist.

Ein Überblick über den traditionellen Beweis lautet wie folgt:

Betrachten Sie einen Satz$\phi$in der Sprache der Mengenlehre, und nehme an, dass NBG'$\vdash \phi$(natürlich alles relativieren, um über Mengen zu quantifizieren).

Ich behaupte, dass ZF$\vdash \phi$.

Betrachten Sie ein Modell$(M, \in_M)$von ZF. Wir können das "Modell der Klassen" konstruieren$(M', \in_{M'})$folgendermaßen:

Zuerst definieren wir$M'$die Sammlung aller Mengen der Form sein$\{x \in M \mid M \models \psi(w_1, \ldots, w_n, x)\}$, Wo$\psi(w_1, \ldots, w_n, x)$ist irgendeine Formel in der Sprache von ZF und$w_1, \ldots, w_n$sind einige Elemente von$M$.

Wir definieren dann$S_1 \in_{M'} S_2$meinen$\exists x \in S_2 (\{y \in M \mid y \in_M x\} = x)$.

Es ist leicht, das zu überprüfen$M'$modelliert alle Axiome von NBG'. Deshalb,$M' \models \phi$nach dem Korrektheitssatz. Das können wir anhand dieser Aussage verifizieren$M \models \phi$.

Da sind alle Modelle von ZF Modelle von$\phi$, können wir aus dem Vollständigkeitssatz schließen, dass ZF$\models \phi$.

Umgekehrt lässt sich leicht zeigen, dass NBG' alle Axiome von ZF beweist. Also wenn ZF$\vdash \phi$, dann NGB'$\vdash \phi$.$\square$

Natürlich sehen wir aus dieser Aussage sofort, dass NBG + Local Choice eine konservative Erweiterung von ZFC ist. Das ist weil$\phi$ist ein Satz von NBG + lokaler Wahl$\iff$ $choice \to \phi$ist ein Satz von NBG'$\iff$ $choice \to \phi$ist ein Satz von ZF$\iff$ $\phi$ist ein Satz von ZFC.

Beachten Sie, dass dieser Beweis auf zwei Tatsachen beruhte: dem Korrektheitssatz für zählbare Vokabulare und dem Vollständigkeitssatz für zählbare Vokabulare. Da diese beiden Sätze in Arithmetik zweiter Ordnung formalisiert werden können, ist es möglich, den obigen Beweis in Arithmetik zweiter Ordnung zu formalisieren (die natürlich erheblich schwächer als ZF ist).

Die Frage ist: Können wir den obigen Beweis nehmen und ihn in Arithmetik erster Ordnung formalisieren?

Es scheint unwahrscheinlich, da wir in der Peano-Arithmetik erster Ordnung keinen rekursiven Wahrheitsbegriff verwenden können. Ich weiß nicht, wie man innerhalb der Peano-Arithmetik überhaupt Fragen zu "Modellen" formulieren könnte.

Wenn wir den obigen Beweis nicht nehmen und ihn in Arithmetik erster Ordnung formalisieren können, gibt es dann einen anderen Beweis, der uns zur Verfügung steht? Ich habe versucht, mit dem Beweis fortzufahren, indem ich boolesche Kategorien als Modelle anstelle von traditionelleren mengentheoretischen Modellen verwendet habe, aber ich bin nicht weitergekommen und bin auf ziemlich dieselben Probleme gestoßen.