Estoy trabajando con el sistema a prueba de FOL se describe en Chang y Keisler. Contiene los siguientes esquemas de axioma:
- $\alpha \to (\beta \to \alpha)$
- $[\alpha\to(\beta\to\gamma)]\to[(\alpha\to\beta)\to(\alpha\to\gamma)]$
- $(\neg\beta\to\neg\alpha)\to(\alpha\to\beta)$
- $\forall x\varphi(x) \to \varphi(t)$ donde $t$ es un término que es gratuito para la sustitución de x en $\varphi$ ($t$ no contiene ninguna variable que va a caer bajo un cuantificador en $\varphi$).
- $\forall x(\varphi \to \psi)\to (\varphi \to \forall x\psi)$ donde $x$ no se producen libremente en $\varphi$.
Las reglas de inferencia son MP (de $\alpha$ $\alpha\to \beta$ inferir $\beta$) y Gen (de $\alpha$ inferir $\forall x \alpha$).
En la prueba del teorema de completitud (página 62 en C&K) llegamos a una etapa en la que algunos la teoría de la $T$ demuestra la siguiente frase:
$$T\vdash \neg[(\exists x)\varphi(x)\to\varphi(d)]$$
Donde $d$ es una constante de símbolos que no están presentes en la teoría. Ahora C&K afirmación de que $$T\vdash [(\exists x)\varphi(x)\wedge \neg\varphi(d)]$$
Esto presenta algunos problemas para mí, como en mi sistema a prueba de $\wedge$ no es formal símbolo (en C&K es, y $\to$ es sólo una forma de taquigrafía). Sin embargo, esto está bien para mí.
Ahora C&K afirmación de que
$$T\vdash \forall x[(\exists x)\varphi(x)\wedge \neg\varphi(x)]$$
Y este es el primer problema real que tengo. Puedo entender la idea detrás de esta afirmación - repita la prueba de la frase anterior sustituir cada ocurrencia de $d$$x$. Sin embargo, estoy no seguro si esto puede llevarse a cabo en el sistema que he descrito.
El principal problema que tengo es con la siguiente afirmación:
$$T\vdash [(\exists x)\varphi(x)\wedge \neg(\exists x)\varphi(x)]$$
Es bastante obvio que esta frase y la anterior fueron semánticamente equivalentes; sin embargo, no veo cómo se puede progresar desde la primera a la segunda en la prueba del sistema que les he descrito. No parece ser cualquier regla pertinente, y mis intentos de "jugar" con las reglas tienen salió con nada.
Mi pregunta es cómo formalizar, en la prueba concreta del sistema me dio (y preferiblemente sin usar $\wedge$) C&K argumento.
(Una respuesta válida es "utilizar otro sistema a prueba", como casi todo libro tiene su propio sabor de un sistema a prueba; sin embargo, prefiero trabajar con "mi" prueba del sistema).
