Sea ZFC2 la formalización de segundo orden de ZFC.
El esquema de comprensión del axioma de segundo orden (parte del sistema deductivo de SOL) dice que para cada fórmula (de SOL) hay una relación con la misma extensión (shapiro 1991).
Si formalizamos ZFC2, entonces el dominio son todos los conjuntos y los cuantificadores de segundo orden abarcan todos los subconjuntos del dominio. Pero entonces, ¿qué impide que surja la paradoja de Russell?
Sé que no es así porque ZFC2 es equivalente a la teoría de conjuntos de Morse-Kelley.
En Lógica de segundo orden , el esquema de comprensión (considerando por simplicidad solo variables predicadas unarias) es:
∃X∀x [ ϕ(x) ↔ X(x) ] ,
donde x es una variable individual , X es una variable predicada 1-aria y X puede no aparecer libre en ϕ .
¿Qué impide que la forma genere la paradoja de Russell ?
Dos hechos:
(i) no podemos sustituir x por x .
Un lenguaje so para conjuntos debe usar variables individuales x para conjuntos y variables predicadas unarias para clases . Entonces, x ∈ A debe formalizarse como A(x) y así, usándolo como ϕ(x) , lo que obtenemos es:
∃X∀x [ ~A(x) ↔ X(x) ] .
(ii) la condición de que X no esté libre en ϕ impide usar ~X(x) para obtener:
∃X∀x [ ~X(x) ↔ X(x) ] .