¿La inconsistencia semántica garantiza la inconsistencia sintáctica?

Question

Estoy pensando en la posibilidad de eludir el problema de incompletitud planteado por Roger Penrose en su libro "Sombras de la mente".

Se me ocurrió (y, al buscar en Google, descubrí que a otros también) que puedes adquirir la completitud de un sistema formal como precio de la consistencia, si adoptas una lógica paraconsistente y un enfoque "falsacionista" mediante el cual tu objetivo sea encontrar subconjuntos consistentes de todas tus proposiciones enumerables. Esto me parece exactamente lo que los seres humanos están haciendo cuando "intuyen" la verdad de la frase gödeliana. Sin embargo, todavía no sé lo suficiente sobre lógica para desarrollar completamente la idea.

En particular, me parece que para que funcione un enfoque falsacionista, necesitas tener $(\Gamma \models \perp) \rightarrow (\Gamma \vdash \perp)$ para garantizar (o al menos hacer muy probable) que eventualmente descubrirás una inconsistencia en tu sistema, si existe.

Parece que para cualquier sistema con un procedimiento efectivo para determinar si $\Gamma \models \phi$ para algún $\phi$, se cumple el requisito ya que para que un procedimiento sea "efectivo" tendría que ser equivalente a algún tipo de manipulación sintáctica de las fórmulas en $\Gamma$.

Además de una respuesta directa estilo "sí", "no", "estás haciendo la pregunta incorrecta", etc., también apreciaría mucho enlaces a la literatura relacionada con el trabajo sobre el problema mencionado anteriormente.

(EDIT) He encontrado otra pregunta que tiene una relación bastante directa con esta, aquí: Teorema de completitud de Gödel y consecuencia lógica

Answer 1

Este es el contenido del teorema de completitud de Gödel. $T\models\varphi$ si y solo si $T\vdash\varphi$, al menos cuando estamos discutiendo lógica de primer orden. Nota, por cierto, que dado que no hay una estructura que satisfaga $\bot$, escribir $T\models\bot$ significa, por definición, que $T$ no tiene modelos.

Interesantemente, esto depende del axioma de elección. Específicamente, la prueba del teorema de completitud utiliza el axioma de elección. Para ver cómo la implicación que te interesa utiliza el axioma de elección, considera el caso en que existe un conjunto $A$ que no puede ser ordenado linealmente (algo que contradice fuertemente el axioma de elección).

Sea $\mathcal L_A$ el lenguaje con constantes $\{c_a\mid a\in A\}$ y un símbolo de relación binaria $<$. Ahora toma $T$ como la teoría que establece que $c_a\neq c_b$ para $a\neq b$ y $<$ es un orden lineal del universo. Esta teoría es finitamente satisfactoria, por lo que no puede demostrar $\bot; pero no tiene modelos, ya que a partir de un modelo de $T$ obtenemos un orden lineal de $A$. (Nota que el lenguaje aquí es innumerable, ya que $A$ es innumerable. Si $\cal L$ es un lenguaje contable en lógica de primer orden, entonces el teorema de completitud para teorías $\cal L$ en realidad es "libre de elección". Por lo tanto, para cosas como la aritmética no usamos el axioma de elección).

Finalmente, permíteme señalar que la incompletitud aquí en el sentido de oraciones godelianas y oraciones Godel-Rosser, no tienen nada que ver con la completitud de la lógica subyacente, o la completitud/coherencia de una teoría. Esos son tipos diferentes de completitud (y falta de ella) y no deben ser confundidos.

Answer 2

Me gustaría agregar otra respuesta a esto centrándome en el caso de los lenguajes contables, ya que ese es el contexto habitual de la lógica y también del argumento de Penrose.

De hecho, la pregunta trata sobre el Teorema de Completitud ($\vdash$ implica $\models$) de la Lógica de Primer Orden, y si siempre es válido. De hecho, mi propia pregunta se preguntaba si este teorema era constructivo, es decir, totalmente efectivo, ya que había estado aprendiendo sobre Matemáticas Reversas y el resultado de que la Completitud dependía de un axioma no constructivo conocido como WKL (Lema débil de Konig). Como tu comentario vinculado muestra, la literatura histórica de la Lógica ha estado confundida sobre la relación entre $\models$ y $\vdash$. Para resumir la razón:

La Lógica de Primer Orden puede ser formalizada en un marco débil llamado RCA que captura la computabilidad. Muchos teoremas (y metateoremas) pueden ser demostrados en RCA, incluido el Teorema de Validez ($\models$ implica $\vdash$) de la Lógica de Primer Orden.

Sin embargo, la Completitud requiere WKL y no es demostrable en RCA.

Una consecuencia inmediata de esto es que $\models$ y $\vdash$ no son intercambiables (a menos que se asuma WKL).

Otra consecuencia es que si una teoría es consistente, no se puede establecer de manera constructiva que tenga un modelo. De hecho, el proceso de construcción de modelos implica un elemento de elección, aunque el Axioma de Elección de ZF no está involucrado. El principio de elección involucrado se menciona en el libro de Matemáticas Reversas y se llama "Elección dependiente fuerte de $\Pi_{1}^{0}$" y es un corolario (meta-) de WKL.

Sin embargo, los modelos parciales pueden construirse de manera constructiva (cuyos elementos son verdaderos o falsos), pero extender esto a todas las propiedades no se puede lograr. Entonces, para cualquier modelo parcial de este tipo, existirá una propiedad p_k tal que p_k(k) se mapeará a {Verdadero, Falso} en nuestro modelo, en lugar de a un valor de verdad específico.

El hecho de que p_k(k) se mapee a {Verdadero, Falso} abre la puerta a lógicas de 3 valores (en las que p_k(k) es indefinido) o a lógicas paraconsistentes (en las que p_k(k) es tanto Verdadero como Falso).

Si uno comienza con una lógica paraconsistente PL, también se ha argumentado que el Teorema de Incompletitud de Gödel no se cumplirá para PL (ya que su demostración requeriría que la inconsistencia sea imposible).

En el argumento de Penrose, en la Inteligencia Artificial y en la Ciencia de la Computación/Ingeniería de Software en general, las lógicas constructivas son fundamentales, aunque la valoración de dos valores, aunque natural y deseable, no se puede garantizar. En cierto sentido, es el axioma WKL el que introduce la valoración de dos valores en toda la lógica, pero lo hace de manera no constructiva, dejando espacio para un debate e investigación mucho más amplios en esta área.