¿Lógica de primer orden en teoría de conjuntos?

Paso 1

Tome cualquier estructura de primer orden$M$sobre cualquier idioma$L$.

Entonces$M$ya interpreta fórmulas sobre$L$, y podemos usar la interpretación. Por ejemplo:

$\forall x,y\ \exists z\ ( z \ne x \land P(x,f(y,z)))$

simplemente se convierte en:

$\forall x,y \in D\ \exists z \in D\ ( z \ne x \land P_M(x,f_M(y,z)))$

dónde$D$es el dominio de$M$y$P_M,f_M$son las interpretaciones de$P,f$en$M$.

Es trivial traducir la aplicación de función y los pares ordenados a ZFC puro, pero no lo haré ya que no vale la pena.

Paso 2

Ahora parece que también quieres deshacerte de los cuantificadores pares.

Tomar cualquiera$1$-sentencia parámetro$φ$sobre ZFC.

Entonces:$\def\none{\varnothing}$

$\forall x \in D\ ( φ(x) )$si y si$\{ x : x \in D \land φ(x) \} = D$.

$\exists x \in D\ ( φ(x) )$si y si$\{ x : x \in D \land φ(x) \} \ne \none$.

Por lo tanto, puede deshacerse recursivamente de los cuantificadores, si permite el uso de constructores de conjuntos, que ZFC puro no tiene.

notas

Si prohíbe los constructores de conjuntos, entonces "$\forall x,y \in D\ ( R_M(x,y) \to R_M(y,x) )$" no se puede traducir a una oración sin cuantificadores, porque cualquier traducción debe afirmar que$R$es simétrico, y no hay forma de hacerlo sin cuantificadores. Tenga en cuenta que la igualdad de conjuntos en sí misma tiene un cuantificador oculto en su interior, que es crucial para permitir que la igualdad entre conjuntos construidos capture afirmaciones cuantificadas.