Esta respuesta se refiere al sistema presentado aquí que es un sistema relativamente típico del estilo Hilbert.
En primer lugar, no se puede utilizar una simple sustitución. Por definición, una sustitución sólo sustituye a las variables libres. Así que si intentas sustituir $y$ para $x$ en $(\exists x)\phi(x)$ se obtiene la misma fórmula $(\exists x)\phi(x)$ . Esta es una convención muy común, y no es en absoluto exclusiva de este autor.
Para demostrar en el sistema particular de este autor que $(\exists x)\phi(x)$ implica $(\exists y)\phi(y)$ , donde $y$ es admisible para $x$ en $\phi$ puede utilizar la regla $L_{15}$ de la siguiente forma: $$ (\forall x)[\phi(x) \to (\exists y)\phi(y)] \to [(\exists x)\phi(x) \to (\exists y)\phi(y)] $$ Esta es una instancia correcta de $L_{15}$ porque en $(\exists y)\phi(y)$ todas las apariciones libres de $x$ en $\phi(x)$ fueron sustituidos por $y$ Así que $x$ no es libre en $(\exists y)\phi(y)$ . Ahora el problema es demostrar que la hipótesis $(\forall x)[\phi(x)\to (\exists y)\phi(y)]$ se puede deducir, porque entonces la conclusión $(\exists x)\phi(x) \to (\exists y)\phi(y)$ se sigue inmediatamente por modus ponens.
Para demostrar $(\forall x)[\phi(x)\to (\exists y)\phi(y)]$ Primero, utilice la regla $L_{13}$ para obtener $\phi(x) \to (\exists y)\phi(y)$ . Esta es una instancia correcta de $L_{13}$ porque $y$ es admisible para $x$ . Ahora utilice la regla de generalización de la página 6 para obtener $(\forall x)[\phi(x)\to (\exists y)\phi(y)]$ .
Muchos sistemas de prueba tienen una regla de inferencia separada, llamada instanciación existencial que dice que desde $(\exists x)\phi(x)$ se puede deducir $\phi(z)$ donde $z$ se elige como una nueva variable que aún no ha aparecido en absoluto en la prueba. En este sistema, la deducción sería la siguiente, en forma simbólica: $$ (\exists x)\phi(x) \Longrightarrow \phi(z) \Longrightarrow (\exists y)\phi(y) $$ donde el segundo $\Longrightarrow$ utiliza la regla $L_{13}$ que funciona porque $z$ se eligió de forma que se garantizara que era admisible para $x$ .
El sistema de prueba adoptado por este autor no admite directamente esta regla, pero es sencillo hacerlo funcionar mediante Skolemización : añade un nuevo símbolo de constante $z_\phi$ a su lenguaje y añadir un axioma lógico $(\forall x)[\phi(x) \to \phi(z_\phi)]$ . Así, $z_\phi$ será un elemento tal que si cualquier elemento satisface $\phi$ entonces $z_\phi$ lo hace. Este axioma no afecta a la consistencia de ninguna teoría a la que se añada, porque cualquier estructura de la teoría original puede ampliarse de forma que el nuevo axioma lógico sea verdadero, y cualquier estructura en la que el sistema ampliado se mantenga satisface automáticamente el sistema original, simplemente ignorando $z_\phi$ . Por lo tanto, utilizando esto y los teoremas de completitud para los sistemas original y expandido, una frase en el lenguaje original es demostrable en el sistema original si y sólo si es demostrable en el sistema expandido.
Ahora la instanciación existencial es una consecuencia inmediata de $L_{15}$ y el nuevo axioma para $z_\phi$ descrito en el párrafo anterior. Como nota histórica, Hilbert desarrolló una idea muy similar que recibe el nombre de $\epsilon$ cálculo . Lo que yo llamo $z_\phi$ se llamaría $(\epsilon x)\phi(x)$ en ese sistema.
La forma en que veo la prueba que describí anteriormente en el sistema original es que se trata de una simulación de instanciación existencial que simplemente evita usar directamente la regla para $z_\phi$ o el $\epsilon$ operador. El coste de evitarlos es que los otros axiomas tienen que ser utilizados de forma menos obvia. De manera informal, $$ (\forall a)[\phi(a) \to \psi] \to [(\exists x) \phi(x) \to \psi] $$ dice que si podemos probar $\phi(a) \to \psi$ para una variable adecuada $a$ entonces podríamos haber demostrado $(\exists x)\phi(x) \to \psi$ . En otras palabras, si queremos demostrar esto último, basta con elegir un $a$ y demostrar lo primero. Esto es análogo a lo que dice la regla de instanciación existencial: dado $(\exists x)\phi(x)$ deberíamos intentar trabajar con $\phi(a)$ en su lugar.
