Esquema axiomático de especificación (argumentos de fórmula)

No necesita parámetros.

Ralf Schindler escribió una breve nota donde se pueden ver los detalles (y Ralf y yo lo discutimos el año pasado alrededor de mayo). Eventualmente encontramos una referencia temprana, que prueba un teorema aún más fuerte. Ver

Azriel Levy, Parámetros en los esquemas de axiomas de comprensión de la teoría de conjuntos , en Actas del simposio de Tarski , Actas de simposios de matemáticas puras, vol. 25, Sociedad Matemática Estadounidense, Providence, RI, págs. 309–324.

(Véase también El elogio del reemplazo de Akihiro Kanamori para una discusión más detallada y referencias adicionales).

El teorema en la nota de Ralf es más fuerte de lo que estás preguntando: podemos formular$\mathsf{ZFC}$sin requerir parámetros ni de comprensión (especificación) ni de reposición.

Como puede ver, el argumento tiene menos de una página. Permítame darle un breve resumen: tenga en cuenta primero que podemos probar la existencia de$0$y$1$, y por tanto de pares ordenados de la forma$(a,0)$o$(a,1)$para cualquier$a$. De (una instancia de reemplazo sin parámetros), obtenemos que$a\times\{0\}$y$a\times\{1\}$existe para cualquier$a$. Asimismo, para cualquier$a$y$b$,$(a\times\{0\})\cup\{(b,1)\}$existe A partir de esto podemos demostrar que

$$\{((u,0),(b,1))\mid u\in a\}$$ existe para cualquier $a$y $b$: Primero, $d=\mathcal P(\mathcal P((a\times\{0\})\cup\{(b,1)\}))$existe, y el conjunto que queremos es $$\{x\in d\mid \exists u\,\exists v\,(x=((u,0),(b,1)))\},$$ que existe aplicando una instancia de especificación sin parámetros.

Ahora podemos probar la especificación con parámetros. Para esto, tenga en cuenta que al usar el emparejamiento, podemos codificar un número finito de parámetros en uno solo, por lo que es suficiente mostrar el resultado para fórmulas con un parámetro, digamos$\phi(x,v)$. Es decir, dado$a,b$, debemos demostrar que

$$\{x\in a\mid \phi(x,b)\}$$ existe

Usamos la instancia de reemplazo sin parámetros dada por la función de clase$F$definido por$F(x)=0$a menos que$x$tiene la forma$((u,0),(c,1))$para algunos$u,c$, en cuyo caso establecemos$F(x)=u$. Vemos eso

$$F''\{((u,0),(b,1))\mid u\in a\}= \{x\in a\mid \phi(x,b)\}\cup\{0\},$$ y de esto sigue su pregunta (aplicando una instancia de especificación sin parámetros para eliminar $0$del conjunto, si es necesario).

Para concluir, demostramos el reemplazo de fórmulas con un parámetro (lo cual nuevamente, por emparejamiento, es suficiente). En consecuencia, deja$\phi(x,y,v)$sea ​​una fórmula, sea$b$Sea un conjunto, y suponga que para cada$x$hay un unico$y$tal que$\phi(x,y,b)$. Debemos demostrar que, para cualquier$a$,

$$\{y\mid\exists x\in a\,(\phi(x,y,b))\}$$ existe

Usamos la instancia de reemplazo sin parámetros dada por la función de clase$F$definido por$F(z)=0$a menos que haya$x,c$con$z=((x,0),(c,1))$, y hay un único$y$tal que$\phi(x,y,c)$se mantiene, en cuyo caso establecemos$F(z)=y$. Entonces vemos que

$$F''\{((x,0),(b,1))\mid x\in a\}=\{y\mid\exists x\in a\,(\phi(x,y,b))\}\cup\{0\}$$ y, como antes, terminamos con una última apelación a una instancia de especificación (sin parámetros), si se elimina $0$del conjunto es necesario.

La necesidad de los cuantificadores universales es un artefacto del hecho de que en las formulaciones clásicas de la lógica el énfasis recae en las proposiciones a las que se les pueden asignar valores de verdad y, por lo tanto, estas proposiciones están necesariamente representadas por fórmulas sin variables libres. En esta configuración, los axiomas, teoremas, etc. son todos necesariamente proposiciones, por lo tanto representados por fórmulas sin variables libres. Por lo tanto, para formular los axiomas en el esquema de axiomas como proposiciones, necesita los cuantificadores universales.

En enfoques menos clásicos (los que se preocupan más por el cálculo de prueba como la teoría de tipos o la teoría de categorías), el énfasis recae en las afirmaciones hipotéticas de que algo es verdadero. Al formular la lógica clásica, tal afirmación puede ser denotada por$\phi\vdash_{\vec x}\psi$, por ejemplo, donde$\phi$y$\psi$son fórmulas arbitrarias, y$\vec x$es una lista que contiene todas las variables libres que ocurren en$\phi$y$\psi$. Esta afirmación debe leerse como: en el contexto de que los símbolos en la lista$\vec x$son elementos del universo de modo que$\phi$Está satisfecho,$\psi$también está satisfecho.

Esta formulación es innecesaria (aunque la encuentro conveniente) para la lógica clásica, ya que la afirmación$\phi\vdash_{\vec x}\psi$es, por la regla de inferencia de implicación equivalente a$\vdash_{\vec x}\phi\rightarrow\psi$(en el contexto$\vec x$, la formula$\phi$implica$\psi$se satisface), lo que es equivalente de la definición del cuantificador universal a$\vdash\forall\vec x(\phi\rightarrow\psi)$(dónde$\forall\vec x$es una abreviatura de$\forall x_1\forall x_2\forall\dots\forall x_n$si$\vec x=[x_1,\dots,x_n]$). Esta afirmación dice que en el contexto vacío, y sin hipótesis, la fórmula (variable libre libre)$\forall\vec x(\phi\rightarrow\psi)$Está satisfecho.

(Tenga en cuenta, sin embargo, que para lógicas no clásicas, o fragmentos de lógica clásica para los que solo se nos otorga acceso restringido a cuantificadores y conectivos, la equivalencia anterior puede simplemente no estar disponible, de ahí esta formulación alternativa).

Así, en particular, en esta formulación alternativa de la lógica clásica, la afirmación

$$\vdash_{\vec w}\forall A \, \exists B \, \forall x \, ( x \in B \leftrightarrow [ x \in A \wedge \varphi] )$$ puede tomarse como un axioma, y ​​es por definición de $\forall$equivalente a la afirmación $$\vdash\forall\vec w(\forall A \, \exists B \, \forall x \, ( x \in B \leftrightarrow [ x \in A \wedge \varphi]$$

Tenga en cuenta que todavía estamos haciendo un seguimiento de las variables libres. Por lo que yo entiendo, no puede no realizar un seguimiento de las variables libres, y parte del enfoque no clásico es que el seguimiento está integrado (ya que si desea tratar con lógica de clasificación múltiple o teoría de tipos, debe tener que realizar un seguimiento no solo de qué símbolos son variables, sino también de qué tipo o tipos son esas variables).

---

Para responder a la pregunta aclarada, simplemente no es cierto en general que cualquier fórmula de dos variables pueda ser reemplazada por una familia infinita de fórmulas de una sola variable. La razón es que los elementos del dominio simplemente no forman parte del alfabeto sobre el que se definen las fórmulas como cadenas de símbolos. En particular para la teoría de conjuntos, las fórmulas son cadenas de símbolos hechos de variables ($x,y,z,\dots$), los conectores lógicos ($\wedge,\vee,\neg,\rightarrow$), los dos cuantificadores ($\exists,\forall$), paréntesis ($(,)$), el signo de igualdad ($=$), y el símbolo de relación no lógica$\in$.

Observe que ni siquiera el conjunto vacío, que denotamos informalmente como$\{\}$, aparece como una expresión en los símbolos anteriores. Más bien, si tenemos una fórmula$\phi(u)$, y queremos instanciarlo con$\{\}$, lo que obtenemos es$\phi_{\{\}}\equiv\left(\forall x\neg(x\in u)\right)\wedge\phi(u)$. En consecuencia, las únicas fórmulas$\phi_z$para$z$un elemento del dominio son aquellos que son definibles , es decir, aquellos que están definidos por la derivabilidad (a partir de los axiomas) de la verdad de una fórmula$\exists z\left(x\in z\leftrightarrow\phi(x)\right)$es cierto donde$\phi$utiliza únicamente los símbolos definidos anteriormente.

Sin embargo, dado que hay muchas fórmulas contables e innumerables conjuntos (este es un resultado metateórico), reemplazando$\phi(x,z)$con$\phi_z(x)$, que solo puedes hacer para definibles$z$, no da como resultado el mismo esquema de axioma: da como resultado el esquema más débil que se refiere solo a conjuntos definibles.

El$w_i$son necesarios. Los criterios de selección$\varphi$puede referirse a variables libres previamente introducidas (la$w_i$) además de$A$.

Ejemplo:

Dejar$A$ser un conjunto.

Suponer$P(w_1,w_2,w_3)$(introduciendo variables libres$w_1,w_2, w_3$usando predicado$P$)

Entonces existe$B\subset A$tal que$\forall x [x\in B \iff x\in A \land\varphi(x,w_1,w_2,w_3,A)]$.

Tenga en cuenta que el subconjunto seleccionado depende de las variables libres$w_1,w_2,w_3$.