¿Se puede probar en Peano Arithmetic el hecho de que NBG sin elección es una extensión conservadora de ZF?

Considere NBG sin elección. Denótese esta teoría NBG'. Es bastante fácil, una vez que uno conoce un poco de teoría de modelos, demostrar que esta teoría es una extensión conservadora de ZF.

Un esquema de la prueba tradicional es el siguiente:

Considere alguna oración$\phi$en el lenguaje de la teoría de conjuntos, y supongamos que NBG'$\vdash \phi$(por supuesto, relativizando todo para cuantificar sobre conjuntos).

Afirmo que ZF$\vdash \phi$.

Por considerar algún modelo$(M, \in_M)$de ZF. Podemos construir el "modelo de clases"$(M', \in_{M'})$como sigue:

Primero, definimos$M'$ser el conjunto de todos los conjuntos de la forma$\{x \in M \mid M \models \psi(w_1, \ldots, w_n, x)\}$, dónde$\psi(w_1, \ldots, w_n, x)$es alguna fórmula en el lenguaje de ZF y$w_1, \ldots, w_n$son algunos elementos de$M$.

Entonces definimos$S_1 \in_{M'} S_2$significar$\exists x \in S_2 (\{y \in M \mid y \in_M x\} = x)$.

Es fácil comprobar que$M'$modela todos los axiomas de NBG'. Por lo tanto,$M' \models \phi$por el teorema de la solidez. Podemos verificar a partir de esta afirmación que$M \models \phi$.

Dado que todos los modelos de ZF son modelos de$\phi$, podemos concluir por el teorema de completitud que ZF$\models \phi$.

A la inversa, se puede demostrar fácilmente que NBG' prueba todos los axiomas de ZF. Entonces si ZF$\vdash \phi$, entonces NGB'$\vdash \phi$.$\square$

Por supuesto, vemos inmediatamente de esta declaración que NBG + opción local es una extensión conservadora de ZFC. Esto es porque$\phi$es un teorema de NBG + elección local$\iff$ $choice \to \phi$es un teorema de NBG'$\iff$ $choice \to \phi$es un teorema de ZF$\iff$ $\phi$es un teorema de ZFC.

Tenga en cuenta que esta prueba se basó en dos hechos: el teorema de solidez para vocabularios contables y el teorema de integridad para vocabularios contables. Debido a que ambos teoremas se pueden formalizar en aritmética de segundo orden, es posible formalizar la prueba anterior en aritmética de segundo orden (que es, por supuesto, considerablemente más débil que ZF).

La pregunta es: ¿podemos tomar la prueba anterior y formalizarla en aritmética de primer orden?

Parece poco probable, ya que no podemos usar una noción recursiva de verdad en la aritmética de Peano de primer orden. No sé cómo se podrían formular preguntas sobre "modelos" dentro de la aritmética de Peano.

Si no podemos tomar la prueba anterior y formalizarla en aritmética de primer orden, ¿hay alguna otra prueba disponible para nosotros? Intenté continuar con la prueba utilizando categorías booleanas como modelos en lugar de modelos teóricos de conjuntos más tradicionales, pero no llegué a ninguna parte y me encontré con los mismos problemas.