Probar la indecidibilidad de la lógica de primer orden sin probarla primero para la aritmética.

Question

Todos los textos que he leído prueban la Indecidibilidad de la lógica de primer orden un poco a posteriori y después de haber probado la incompletitud e Indecidibilidad de la Aritmética (de Peano).

Esta prueba tampoco funciona en filosofía, me gustaría una prueba de que la lógica de primer orden es indecidible, pero sin usar la aritmética, los teoremas de incompletitud de Godels y todo eso.

Es un camino tan tortuoso y que muchos se perderán a mitad de camino, se trata de lógica de primer orden ¿por qué necesitamos añadir aritmética para probar la indecidibilidad?

Mis primeras ideas de una prueba:

(no estoy seguro de que sea correcto, ya publiqué esto antes de forma un poco diferente en , Teorema de completitud de Gödel y satisfabilidad de una fórmula en lógica de primer orden (en espera de comentarios)

• Hay algunas fórmulas en las que la respuesta sobre la validez depende de la tamaño del dominio.

$\exists x R(x) \to \forall x R(x) $ es verdadero cuando el dominio sólo contiene un elemento, pero falso en cualquier dominio mayor.

Supongamos que ahora tenemos una fórmula $\phi $ que es falso en todo dominio finito pero es verdadero en un dominio infinito.

• No podemos construir un modelo de $\phi $ sólo porque requiere un dominio infinito.
• Tampoco podemos probar $\lnot \phi $ porque simplemente no es una afirmación verdadera

Así que por solidez $ \not \vdash \lnot \phi $ y también $ \phi $ no tiene un modelo finito (construible) por lo que $ \phi $ y $\lnot \phi $ son afirmaciones indecidibles

Y para $\phi $ podemos usar simplemente $\lnot ( \forall x \forall y \forall z (((Rxy \land Ryz) \to Rxz ) \land \lnot Rxx) \land \forall y \exists x Rxy )$

Estoy de acuerdo $\phi $ es una especie de aritmética (mínima) disfrazada, interpreta Rxy como $ x > y $ pero no es aritmética completa y la prueba es mucho más corta.

Pero, ¿es este un razonamiento correcto?

¿Tiene un modelo para ser constructivo? ( $ \phi $ es "obviamente" satisfacible sólo que no es construible)

¿Hay otras y mejores formas de explicarlo? (las referencias son muy bienvenidas)

Answer 1

Me gustaría una prueba de que la lógica de primer orden es indecidible, pero sin usar la aritmética

Pero, ¡agárrense! La proposición "la lógica de primer orden es indecidible" es, cuando se descompone, sólo una proposición de la forma "no hay ninguna función computable que haga tal y tal cosa". Así que por supuesto una prueba de esta proposición va a tener que venir de una aplicación de la teoría general de las funciones computables. (Puede que sólo necesitemos una capacidad ingenua para reconocer un cálculo cuando lo veamos para establecer la afirmación positiva de que alguna función puede computar: pero para establecer una negativa, que hay no función computable que hace tal o cual cosa, necesitamos alguna teoría general que nos permita hablar de los límites de lo computable).

Ahora bien, los cálculos relevantes aquí son sobre cadenas finitas que constituyen wffs y pruebas, por lo que la teoría de fondo que necesitamos de hecho es o equivale a la teoría de las funciones aritméticas computables (ya que se pueden codificar cadenas finitas mediante números de manera familiar; o de hecho podemos ir en la dirección opuesta y reconstruir la aritmética en la teoría de las cadenas finitas). Así que las líneas naturales de prueba de que la lógica de primer orden es indecidible vendrán de la teoría de las funciones aritméticas computables (quizás con un ligero disfraz) . En resumen, las consideraciones ampliamente aritméticas (lejos de ser extrañas, un desvío "tortuoso") son exactamente lo que esperaríamos usar aquí.

---

Añadido: Lo que escribí más arriba era [al menos pretendía ser] coherente con el tipo de puntos que Carl Mummert expone en su típica y elegante respuesta. Es la teoría de la computabilidad la que necesita ser invocada: pero el punto en el que se aplica no tiene por qué ser una aritmética formal. Como Carl señala muy bien, podríamos pasar por la prueba de Tarksi sobre los grupos. Sin embargo, yo estaba entendiendo que ese tipo de cosas le parecerían a la OP un camino aún más "tortuoso" para llegar al resultado de indecidibilidad; y todavía estamos aplicando la teoría de las funciones numéricas computables.

---

Este es el punto principal, pero quizá pueda añadir un comentario subsidiario sobre la observación

No podemos construir un modelo de ϕ sólo porque requiere un dominio infinito.

Bueno, según cualquier estándar constructivo ordinario, el wff que describes (perdiendo la negación no intencionada) tiene un modelo constructivamente aceptable -- ¡los números naturales en su orden natural! ¿Qué hay de malo en ello?

Answer 2

Sí, es posible demostrar la indecidibilidad de la lógica de primer orden sin la aritmética formal. Al final, la indecibilidad se refiere sobre todo a la teoría de la computabilidad.

Por ejemplo, Tarski demostró que la teoría de grupos es indecidible: no hay ningún procedimiento para decidir si una fórmula $\phi$ en el lenguaje de los grupos es demostrable a partir de los axiomas de grupo. Pero los axiomas de grupo son de número finito, por lo que podemos escribirlos como un solo axioma $G$ . Entonces se deduce del resultado de Tarski que no debe haber ningún procedimiento para determinar si una frase de la forma $G \to \phi$ es demostrable (sin axiomas adicionales), cuando $\phi$ está en el lenguaje de los grupos. Así, en general, la demostrabilidad de primer orden no es decidible.

La prueba de Tarski funciona mostrando que la teoría de grupos puede utilizarse para codificar hechos sobre la computación, de modo que decidir qué sentencias sobre grupos son demostrables nos permitiría resolver el problema de la parada. Pero la prueba de Tarski no requiere nada sobre la aritmética formal.

Lo que obtenemos de la aritmética formal es una propiedad más fuerte. Teorías como la aritmética de Peano son esencialmente indecidible no sólo es indecidible la aritmética de Peano, sino que cualquier extensión consistente y efectivamente axiomatizada de la aritmética de Peano es también indecidible. Este no es el caso de la teoría de grupos. Si añadimos $(\forall x)(\forall y)[x=y]$ a los axiomas de grupo, obtenemos la teoría de un grupo de un elemento, que es decidible.

Answer 3

En realidad, debería ser posible probar la indecidibilidad de la lógica de primer orden sin ninguna teoría de fondo, así que sólo en la lógica simple, por reducción al Problema de la Parada (en realidad, Turing y Church hicieron esto, en mi opinión). Echa un vistazo a esto página web de la universidad de Stanford .

Answer 4

Me gustaría añadir algunas reflexiones sobre el tema de la "no constructividad", relacionando algunos posts anteriores sobre El Teorema de Completitud de Gödel y la satisfabilidad y Contenido matemático del Teorema de Completitud de Gödel y Roy Simpson Constructividad del Teorema de Completitud de Gödel .

Mis reflexiones son las siguientes :

(i) Pruebas modernas del Teorema de Gödel

Creo que los de la tradición de Gentzen están más "en el espíritu" de la prueba original de G.

Referencias a teoría de la prueba libros de texto :

• Kurt Schutte, Teoría de la prueba (traducción inglesa 1977 - 1ª ed. alemana 1960), ver página 29,

• Gaisi Takeuti, Teoría de la prueba (2ª ed. 1987 - 1ª ed. 1975), véase la página 40,

• Sara Negri y Jan von Plato, Teoría de la prueba estructural (2001), véase la página 81,

y mi "amada" : S.C.Kleene, Lógica matemática (1967) y R.Smullyan, Lógica de primer orden (1969).

En primer lugar, relacionan claramente el teorema con un sistemas de prueba (este es mi sentimiento "muy personal": No me gustan las pruebas que validan el teorema sin ninguna mención a un sistema de pruebas).

En segundo lugar, debido al "origen hilbertiano" de teoría de la prueba son muy sensibles a la hora de declarar los "recursos matemáticos" necesarios en la demostración (lema de König); véase Schutte, página 30.

La prueba [...] no es constructiva ya que se basa en las nociones no constructivas de validez y en el lema de König, que tiene una prueba no constructiva.

En tercer lugar, en la construcción de la prueba, construyen un árbol que es

definida constructivamente y se deduce de la prueba que para cada fórmula deducible se tiene una deducción estándar que viene dada, constructivamente, por el [árbol].

de nuevo desde el Nota: en el libro de texto de Schutte, página 32.

---

(ii) Validez y dominios infinitos

Suponiendo que las reflexiones anteriores sean correctas, añadiré, siguiendo la nota de Peter Smith sobre Argumentos para exprimirse (2010), que las pruebas anteriores relacionan claramente las nociones de "validez-en-virtud-de-forma", como se definió durante los años 20 en la escuela de Hilbert, desde Bernays hasta el artículo de Gödel de 1930, con la noción de "derivabilidad-en-un-sistema-de-prueba" y con la noción de "tener un contramodelo en los números naturales", todos los cuales son los "ingredientes básicos" de la prueba original de Gödel.

Dicho esto, pregunto por el "compromiso ontológico" de la prueba anterior.

Podemos prescindir de $\mathsf {ZFC}$ ?

En realidad sólo necesitamos el lema de König, los números naturales y la inducción.

Basta con algunos subsistemas débiles de la aritmética de segundo orden para formalizar esta pieza matemática?

Según alguna respuesta anterior de Carl Mummert, $\mathsf {WKL_0}$ es suficiente.

Según las palabras del OP "la respuesta sobre la validez depende del tamaño del dominio": cierto. Pero si dejamos el dominio infinito de los números naturales (es decir $\mathbb {N}$ ) perdemos cualquier "interés" en la lógica de predicados.

Si asumo una limitación a los dominios finitos, puedo prescindir totalmente de los cuantificadores y quedarme con las conjunciones y disyunciones finitas; así lógica proposicional es suficiente, y tenemos decidibilidad y métodos eficaces (como la tabla de verdad) para comprobar la validez.