Decidibilidad (lógica)

En lógica , un problema de decisión verdadero/falso es decidible si existe un método efectivo para obtener la respuesta correcta. Los sistemas lógicos son decidibles si la pertenencia a su conjunto de fórmulas (o teoremas) lógicamente válidas puede determinarse de manera efectiva. La lógica de orden cero (lógica proposicional) es decidible, mientras que la lógica de primer orden y las de orden superior no lo son. Una teoría (conjunto de enunciados cerrados bajo consecuencia lógica ) en un sistema lógico fijo es decidible si existe un método efectivo para determinar si fórmulas arbitrarias están incluidas en la teoría. Muchos problemas importantes son indecidibles ; es decir, se ha demostrado que no existe un método efectivo para determinar la pertenencia (que devuelva una respuesta correcta después de un tiempo finito, aunque posiblemente muy largo, en todos los casos).

Cada sistema lógico posee un componente sintáctico , que entre otras cosas determina la noción de demostrabilidad , y un componente semántico , que determina la noción de validez lógica . Las fórmulas lógicamente válidas de un sistema se denominan a veces teoremas del sistema, especialmente en el contexto de la lógica de primer orden, donde el teorema de completitud de Gödel establece la equivalencia entre consecuencia semántica y sintáctica. En otros contextos, como la lógica lineal , la relación de consecuencia sintáctica (demostrabilidad) puede utilizarse para definir los teoremas de un sistema.

Un sistema lógico es decidible si existe un método eficaz para determinar si determinadas fórmulas son teoremas de dicho sistema. Por ejemplo, la lógica proposicional es decidible, ya que el método de las tablas de verdad permite determinar si una fórmula proposicional arbitraria es lógicamente válida.

La lógica de primer orden no es decidible en general; en particular, el conjunto de validez lógica en cualquier signatura que incluya igualdad y al menos otro símbolo de predicado con dos o más argumentos no es decidible. ^{[ 1 ]} Los sistemas lógicos que extienden la lógica de primer orden, como la lógica de segundo orden y la teoría de tipos , también son indecidibles.

Sin embargo, la validez del cálculo de predicados monádicos con identidad es decidible. Este sistema es lógica de primer orden restringida a aquellas signaturas que no tienen símbolos de función y cuyos símbolos de predicado, distintos de la igualdad, nunca toman más de un argumento.

Algunos sistemas lógicos no se representan adecuadamente solo con el conjunto de teoremas. (Por ejemplo, la lógica de Kleene no tiene ningún teorema). En tales casos, se suelen utilizar definiciones alternativas de decidibilidad de un sistema lógico, que requieren un método eficaz para determinar algo más general que la mera validez de las fórmulas; por ejemplo, la validez de las secuencias o la relación de consecuencia {(Г, A ) | Г ⊧ A } de la lógica.

Una teoría es un conjunto de fórmulas, que a menudo se asumen cerradas bajo consecuencias lógicas . La decidibilidad de una teoría se refiere a si existe un procedimiento efectivo que decida si una fórmula pertenece o no a la teoría, dada una fórmula arbitraria en la signatura de la misma. El problema de la decidibilidad surge naturalmente cuando una teoría se define como el conjunto de consecuencias lógicas de un conjunto fijo de axiomas .

Existen varios resultados básicos sobre la decidibilidad de las teorías. Toda teoría inconsistente (no paraconsistente ) es decidible, ya que toda fórmula en su signatura será una consecuencia lógica y, por lo tanto, un miembro de la misma. Toda teoría de primer orden completa y computacionalmente enumerable es decidible. Una extensión de una teoría decidible puede no serlo. Por ejemplo, existen teorías indecidibles en lógica proposicional, aunque el conjunto de validez (la teoría más pequeña) sea decidible.

Una teoría consistente que posee la propiedad de que toda extensión consistente es indecidible se denomina esencialmente indecidible . De hecho, toda extensión consistente será esencialmente indecidible. La teoría de cuerpos es indecidible, pero no esencialmente indecidible. Se sabe que la aritmética de Robinson es esencialmente indecidible, por lo que toda teoría consistente que incluya o interprete la aritmética de Robinson también es (esencialmente) indecidible.

Entre los ejemplos de teorías decidibles de primer orden se incluyen la teoría de los cuerpos reales cerrados y la aritmética de Presburger , mientras que la teoría de grupos y la aritmética de Robinson son ejemplos de teorías indecidibles.

Algunas teorías decidibles incluyen (Monk 1976, p.  234): ^{[ 2 ]}

• El conjunto de validez lógica de primer orden en la signatura con solo igualdad, establecido por Leopold Löwenheim en 1915.
• El conjunto de validez lógica de primer orden en una signatura con igualdad y una función unaria, establecido por Ehrenfeucht en 1959.
• La teoría de primer orden de los números naturales en signatura con igualdad y suma, también llamada aritmética de Presburger . Su completitud fue establecida por Mojżesz Presburger en 1929.
• La teoría de primer orden de los números naturales en signatura con igualdad y multiplicación, también llamada aritmética de Skolem .
• La teoría de primer orden de las álgebras booleanas , establecida por Alfred Tarski en 1940 (descubierta en 1940 pero anunciada en 1949).
• La teoría de primer orden de cuerpos algebraicamente cerrados de una característica dada , establecida por Tarski en 1949.
• La teoría de primer orden de campos ordenados reales cerrados , establecida por Tarski en 1949 (véase también el problema de la función exponencial de Tarski ).
• La teoría de primer orden de la geometría euclidiana , establecida por Tarski en 1949.
• La teoría de primer orden de los grupos abelianos , establecida por Szmielew en 1955.
• La teoría de primer orden de la geometría hiperbólica , establecida por Schwabhäuser en 1959.
• Sublenguajes decidibles específicos de la teoría de conjuntos investigados desde la década de 1980 hasta la actualidad. (Cantone et al. , 2001)
• La teoría monádica de segundo orden de los árboles (véase S2S ).

Los métodos utilizados para establecer la decidibilidad incluyen la eliminación de cuantificadores , la completitud del modelo y la prueba de Łoś–Vaught .

Algunas teorías indecidibles incluyen: ^{[ 2 ]}

• El conjunto de validez lógica en cualquier signatura de primer orden con igualdad y que cumpla con alguna de las siguientes condiciones: un símbolo de predicado de aridad no menor que 2, o dos símbolos de función unaria, o un símbolo de función de aridad no menor que 2, establecido por Trakhtenbrot en 1953.
• La teoría de primer orden de los números naturales con suma, multiplicación e igualdad, establecida por Tarski y Andrzej Mostowski en 1949.
• La teoría de primer orden de los números racionales con suma, multiplicación e igualdad, establecida por Julia Robinson en 1949.
• La teoría de grupos de primer orden , establecida por Alfred Tarski en 1953. ^{[ 3 ]} Sorprendentemente, no solo la teoría general de grupos es indecidible, sino también varias teorías más específicas, por ejemplo (como estableció Mal'cev en 1961) la teoría de grupos finitos . Mal'cev también estableció que la teoría de semigrupos y la teoría de anillos son indecidibles. Robinson estableció en 1949 que la teoría de cuerpos es indecidible.
• La aritmética de Robinson (y, por lo tanto, cualquier extensión consistente, como la aritmética de Peano ) es esencialmente indecidible, como estableció Raphael Robinson en 1950.
• La teoría de primer orden con igualdad y dos símbolos de función. ^{[ 4 ]}

El método de interpretabilidad se utiliza a menudo para establecer la indecidibilidad de las teorías. Si una teoría T esencialmente indecidible es interpretable en una teoría consistente S , entonces S también es esencialmente indecidible. Esto está estrechamente relacionado con el concepto de reducción muchos a uno en la teoría de la computabilidad .

Una propiedad de una teoría o sistema lógico más débil que la decidibilidad es la semidecidibilidad . Una teoría es semidecidible si existe un método bien definido cuyo resultado, dada una fórmula arbitraria, es positivo si la fórmula pertenece a la teoría; de lo contrario, puede que nunca se obtenga o que el resultado sea negativo. De forma equivalente, un sistema lógico es semidecidible si existe un método bien definido para generar una secuencia de teoremas de tal manera que cada teorema se genere finalmente. Esto difiere de la decidibilidad porque en un sistema semidecidible puede que no exista un procedimiento eficaz para comprobar que una fórmula no es un teorema.

Toda teoría o sistema lógico decidible es semidecidible, pero en general no se cumple lo contrario; una teoría es decidible si y solo si tanto ella como su complemento son semidecidibles. Por ejemplo, el conjunto de validez lógica V de la lógica de primer orden es semidecidible, pero no decidible. En este caso, se debe a que no existe un método efectivo para determinar, para una fórmula arbitraria A, si A no pertenece a V. De manera similar, el conjunto de consecuencias lógicas de cualquier conjunto de axiomas de primer orden computablemente enumerable es semidecidible. Muchos de los ejemplos de teorías de primer orden indecidibles mencionados anteriormente son de esta forma.

La decidibilidad no debe confundirse con la completitud . Por ejemplo, la teoría de los cuerpos algebraicamente cerrados es decidible pero incompleta, mientras que el conjunto de todas las proposiciones verdaderas de primer orden sobre los números naturales en el lenguaje con + y × es completo pero indecidible. Desafortunadamente, debido a una ambigüedad terminológica, el término "proposición indecidible" se usa a veces como sinónimo de proposición independiente .

Al igual que con el concepto de conjunto decidible , la definición de una teoría o sistema lógico decidible puede expresarse en términos de métodos efectivos o de funciones computables . Según la tesis de Church , estos enfoques se consideran generalmente equivalentes . De hecho, la demostración de que un sistema o teoría lógica es indecidible utilizará la definición formal de computabilidad para demostrar que un conjunto apropiado no es decidible, y luego recurrirá a la tesis de Church para demostrar que la teoría o el sistema lógico no es decidible mediante ningún método efectivo (Enderton 2001, págs.  206 y ss. ).

Algunos juegos se han clasificado según su capacidad de decisión:

• El jaque mate en n en ajedrez infinito (con limitaciones en las reglas y las piezas) es decidible. ^{[ 5 ] [ 6 ]} Sin embargo, existen posiciones (con un número finito de piezas) que son victorias forzadas, pero no jaque mate en n para ningún n finito . ^{[ 7 ]}
• Algunos juegos de equipo con información imperfecta en un tablero finito (pero con tiempo ilimitado) son indecidibles. ^{[ 8 ]}

• Problema de decisión
• cuantificación existencial