Pregunta sobre la prueba lógica de primer orden

Question

No tengo ni idea de cómo empezar a construir esta prueba, ¡y agradecería cualquier ayuda!

Tengo que demostrar lo siguiente, y para más inri, sin solidez ni plenitud:

$$ \vdash (\forall x. \phi) \rightarrow (\exists x.\phi)$$

Puedo utilizar los siguientes axiomas/teoremas:

Ax1 $\langle \forall^\ast (\varphi \rightarrow (\psi \rightarrow \varphi)) \rangle$ ;

Ax2 $\langle \forall^ ((\varphi \rightarrow (\psi \rightarrow \eta)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \eta))) \rangle$ ;

Ax3 $\langle \forall^ (((\neg \varphi) \rightarrow (\neg \psi)) \rightarrow (\psi \rightarrow \varphi)) \rangle$ ;

Ax4 $\langle \forall^\ast (\forall x.(\varphi \rightarrow \psi)) \rightarrow ((\forall x. \varphi) \rightarrow (\forall x. \psi)) \rangle$ ;

Ax5 $\langle \forall^\ast (\forall x. \varphi) \rightarrow \varphi^x_t \rangle$ para $t \in \rm{TS}$ un término;

Ax6 $\langle \forall^\ast (\varphi \rightarrow \forall x.\varphi) \rangle$ para $x \notin \operatorname{FV}(\varphi)$ y

MP $\langle \varphi, (\varphi \rightarrow \psi), \psi \rangle$ .

y el lema "Que $\Sigma \vdash \varphi$ y $x \notin \operatorname{FV}(\Sigma)$ . Entonces $\Sigma \vdash \forall x. \varphi$ ."

Gracias.

---

EDIT [SN]: La pregunta original no mencionaba el lema en la última línea. Lo he añadido basándome en otra pregunta que por lo demás es un duplicado exacto de esto.

Answer 1

Como menciono en mi respuesta a la otra pregunta Si sus axiomas son todas oraciones (de modo que los cuantificadores universales cuantifican sobre todas las variables que aparecen) y si no hay símbolos constantes en su lenguaje, entonces es imposible hacer la deducción, ya que los axiomas son todos verdaderos en la estructura vacía y la regla de inferencia es válida para esta estructura, pero la deducción deseada no es válida en la estructura vacía.

Así que permíteme suponer que no pretendes que los axiomas estén totalmente cuantificados universalmente, y los comentarios de la otra pregunta sugieren esta lectura.

Permítanme primero dar una deducción en un sistema modificado, donde modificamos el axioma 3 para afirmar $\langle \forall^∗ ((\varphi \rightarrow (\neg \psi)) \rightarrow (\psi \rightarrow \neg\varphi)) \rangle$ que es similar y simplemente coloca las negaciones en lugares ligeramente diferentes. Con este axioma modificado, uno puede hacer la deducción como sigue:

• $\forall x.\varphi(x)$ . Supongamos por hipótesis.
• $[\forall x.\varphi(x)]\to \varphi(t)$ Utilizando cualquier plazo fijo $t$ . Por el axioma 5.
• $\varphi(t)$ . Por modus ponens.
• $[\forall x.\neg\varphi(x)]\to \neg\varphi(t)$ . Por el axioma 5.
• $[[\forall x.\neg\varphi(x)]\to \neg\varphi(t)]\to [\varphi(t)\to \neg\forall x.\neg\varphi(x)]$ . Este es un caso del axioma 3 modificado.
• $\varphi(t)\to \neg\forall x.\neg\varphi(x)$ . Por modus ponens.
• $\neg\forall x.\neg\varphi(x)$ . Por modus ponens.
• $\exists x.\varphi(x)$ . Por definición de $\exists$ .

Así, tenemos $\forall x.\varphi(x)\vdash\exists x.\varphi(x)$ y así por el teorema de la deducción, $\vdash\forall x.\varphi(x)\to\exists x.\varphi(x)$ , según se desee.

Ahora, en lugar de modificar el axioma 3, se puede deducir, si se sabe que $\vdash\neg\neg\varphi\to\varphi$ . La razón es que para mostrar $A\to\neg B\vdash B\to\neg A$ basta con mostrar $A\to\neg B,B\vdash\neg A$ pero uno tiene $\vdash(\neg\neg A\to \neg B)\to(B\to \neg A)$ por el axioma 3 original, por lo que ahora utilizamos el hecho de que $\vdash\neg\neg A\to A$ para conseguirlo en unos pocos pasos.

Por supuesto, queremos $\vdash\neg\neg\varphi\to\varphi$ ser el caso, pero confieso que mirándolo brevemente ahora mismo no veo inmediatamente cómo hacerlo en el sistema que has especificado. Uno podría simplemente añadirlo como un axioma, pero tal vez haya una forma inteligente de deducirlo.

Answer 2

El teorema ya es válido en la lógica mínima. Significa que no se necesita ni ~ ~ A -> A ni algo equivalente (por ejemplo Ax3 en el post) que se sitúe entre la lógica mínima y la lógica clásica. Aquí hay una demostración en lógica mínima, estoy usando A -> f para ~A.

 1) A(y) |- A(y) (Id)

 2) f |- f (Id)

 3) A(y) , A(y) -> f |- f (Left -> 1+2)

 4) A(y), forall x(A(x) -> f) |- f (Left forall 3)

 5) forall x A(x), forall x (A(x) -> f) |- f (Left forall 4)

 6) forall x A(x) |- forall x (A(x) -> f) -> f (Right -> 5)

 7) |- forall x A(x) -> (forall x (A(x) -> f) -> f) (Right -> 6)

Lo anterior es una prueba de Gentzen. Pero el cartel dio un cálculo al estilo de Hilbert. Podemos convertir la prueba anterior en una prueba de estilo Hilbert con los axiomas del cartel. Supongo que será un poco más larga que la prueba de Genzten. Pero no hará uso de Ax3.

Saludos cordiales