¿Puede la lógica de primer orden pura ser axiomatizada por una lista recursiva de declaraciones?

Question

Si cada línea de una prueba debe ser una afirmación y no simplemente una fórmula bien formada (wff), ¿algún conjunto recursivo de axiomas implica todas las afirmaciones válidas en lógica de primer orden pura? Supongo que una respuesta en broma sería "Sí, porque el conjunto de todas las afirmaciones válidas en lógica de primer orden pura es recursivamente enumerable, y un teorema de Craig dice que hay una axiomatización recursiva de cualquier teoría con una axiomatización recursivamente enumerable." Pero quiero una lista práctica de axiomas que realmente pueda escribir.

Debo señalar que hago esta pregunta porque estoy tratando de evitar un problema que tengo al entender la noción de prueba de Enderton. Específicamente, realmente no sé qué significa que una fórmula bien formada que no es una afirmación sea un axioma o una línea intermedia en una prueba.

Answer 1

Este es mi primer intento de responder a una pregunta, así que haré mi mejor esfuerzo.

En primer lugar, es importante entender qué representa una variable libre en una fórmula.

Cuando hablamos de axiomas (como lo hace Enderton) estamos hablando de un conjunto de fórmulas que, mediante reglas de derivación, pueden darnos nuevas fórmulas. Estos axiomas, sin embargo, se establecen usando metavariables. Por ejemplo, $\varphi \rightarrow (\psi \rightarrow \chi) \rightarrow ((\varphi\rightarrow\psi) \rightarrow (\varphi\rightarrow\psi))$. Estas metavariables representan otras fórmulas que se pueden "insertar" para que tengas nuevas instancias del mismo axioma.

Al introducir la noción de prueba, la idea es que cualquier nueva fórmula se deriva ya sea por aplicación del Modus Ponens a una fórmula ya derivada, o una instancia del axioma o por uso de alguna de las reglas de derivación. Al decir que una fórmula que no es una declaración es un axioma, estás instanciando uno de los axiomas, pero insertando variables que no están cuantificadas. En principio, esto no sería un problema: puedes operar con fórmulas abiertas, sin embargo se necesita cierta precaución.

Existe un axioma que dice que se puede cerrar una fórmula que tiene variables libres agregando un cuantificador universal para cada variable libre existente en la fórmula. Así, si durante tu prueba llegas a una fórmula, digamos, $\vdash\varphi(x,y)$, donde $x,y$ son variables libres, entonces es posible cerrar esta fórmula agregando un cuantificador universal para cada variable en el orden de aparición, es decir, $\vdash\forall y \forall x \varphi(x,y)$. Por lo tanto, tener una fórmula que no es una declaración como un axioma o una línea en una prueba simplemente significa que hay una instancia de una fórmula que aún no se ha cerrado.