La necesidad de los cuantificadores universal es un artefacto del hecho de que en las formulaciones clásicas de la lógica, el énfasis cae sobre las proposiciones que podría tener la verdad de los valores asignados a ellos, y por lo tanto, estas proposiciones son necesariamente representados por las fórmulas sin variables libres. En este conjunto, axiomas, teoremas, etc. son todos necesariamente proposiciones, de ahí representados por las fórmulas sin variables libres. Por lo tanto, para la formulación de los axiomas en el axioma esquema de proposiciones, usted necesita el universal cuantificadores.
En menos enfoques clásicos (los más interesados en la prueba de cálculo como el tipo de teoría, o la categoría de la teoría), el énfasis cae sobre la hipotética afirmaciones de que algo es verdadero. Cuando la formulación de la lógica clásica, tal afirmación puede ser denotado por $\phi\vdash_{\vec x}\psi$, por ejemplo, donde $\phi$ $\psi$ son arbitrarias fórmulas, y $\vec x$ es una lista que contiene todas las variables libres se producen en $\phi$$\psi$. Esta afirmación debe entenderse como: en el contexto de que los símbolos en la lista de $\vec x$ son los elementos del universo, de modo que $\phi$ está satisfecho, $\psi$ también está satisfecho.
Esta formulación es innecesario (aunque me parece conveniente) para la lógica clásica, desde la afirmación de $\phi\vdash_{\vec x}\psi$ es, por la regla de inferencia de la implicación equivalente a $\vdash_{\vec x}\phi\rightarrow\psi$ (en el contexto de $\vec x$, la fórmula $\phi$ implica $\psi$ está satisfecho), que es equivalente a partir de la definición de la universal quantifierto $\vdash\forall\vec x(\phi\rightarrow\psi)$ (donde $\forall\vec x$ es una abreviatura para $\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 vacío contexto, y con ninguna hipótesis, la (variable libre libre) fórmula $\forall\vec x(\phi\rightarrow\psi)$ está satisfecho.
(Tenga en cuenta, sin embargo, que para los no-clásica de la lógica, o fragmentos de la lógica clásica para la que se nos ha concedido un acceso restringido a los cuantificadores y las conectivas, por encima de la equivalencia puede simplemente no estar disponibles, por lo tanto, esta formulación alternativa).
Así, en particular, en esta alternativa la formulación de la lógica clásica, la afirmación de $$\vdash_{\vec w}\forall A \, \exists B \, \forall x \, ( x \in B \leftrightarrow [ x \in A \wedge \varphi] )$$ can be taken as an axiom, and is by definition of $\forall$ equivalent to the assertion $$\vdash\forall\vec w(\forall A \, \exists B \, \forall x \, ( x \in B \leftrightarrow [ x \in A \wedge \varphi] $$
Aviso de que se está manteniendo un seguimiento de las variables libres. Como tengo entendido, no puedes dejar de seguir la pista de las variables libres, y parte de la no-clásico enfoque es que el seguimiento está integrado (ya que si usted quiere tratar con múltiples ordenados lógica o tipo de teoría, usted tiene que seguir no sólo de que los símbolos son variables, pero también de qué tipo o tipos de esas variables).
Para responder a la aclarado la pregunta, no es cierto en general que cualquiera de las dos variables de la fórmula puede ser sustituida por una familia infinita de variables simples fórmulas. La razón es que los elementos del dominio, simplemente, no son parte del alfabeto sobre el que las fórmulas son definidos como cadenas de símbolos. En particular, para la teoría de conjuntos, las fórmulas son cadenas de símbolos hecho de variables ($x,y,z,\dots$), los conectivos lógicos ($\wedge,\vee,\neg,\rightarrow$), los dos cuantificadores ($\exists,\forall$), los paréntesis ($(,)$), el signo de igualdad ($=$), y la no-relación lógica símbolo $\in$.
Aviso que ni siquiera es el conjunto vacío, que podemos denotar de manera informal como $\{\}$, se produce como una expresión en la anterior los símbolos. Más bien, si tenemos una fórmula $\phi(u)$, y queremos crear una instancia con $\{\}$, lo que obtenemos es $\phi_{\{\}}\equiv\left(\forall x\neg(x\in u)\right)\wedge\phi(u)$. En consecuencia, la única fórmulas de $\phi_z$ $z$ un elemento del dominio son aquellos que son definibles, es decir, aquellas que son definidas por el derivability (a partir de los axiomas) de la verdad de una fórmula $\exists z\left(x\in z\leftrightarrow\phi(x)\right)$ es cierto en lo que a $\phi$ sólo utiliza los símbolos definidos anteriormente.
Sin embargo, ya que hay countably muchas fórmulas, y una cantidad no numerable de conjuntos (esto es un metatheoretical resultado), en sustitución de $\phi(x,z)$$\phi_z(x)$, que sólo se puede hacer por definibles $z$, no da como resultado el mismo axioma esquema: es el resultado del más débil esquema de que sólo se refiere a conjuntos definibles.
