Decidibilidad (lógica)

En lógica , un problema de decisión verdadero/falso es decidible si existe un método efectivo para derivar la respuesta correcta. La lógica de orden cero (lógica proposicional) es decidible, mientras que la lógica de primer orden y de orden superior no lo son. Los sistemas lógicos son decidibles si la pertenencia a su conjunto de fórmulas (o teoremas) lógicamente válidas se puede determinar de manera efectiva. Una teoría (conjunto de oraciones cerradas bajo consecuencia lógica ) en un sistema lógico fijo es decidible si existe un método efectivo para determinar si se incluyen fórmulas arbitrarias en la teoría. Muchos problemas importantes son indecidibles , es decir, se ha demostrado que no puede existir 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) para ellos.

Cada sistema lógico tiene 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 a veces se denominan 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 de la consecuencia semántica y sintáctica. En otros entornos, como la lógica lineal , la relación de consecuencia sintáctica (demostrabilidad) puede usarse para definir los teoremas de un sistema.

Un sistema lógico es decidible si existe un método eficaz para determinar si fórmulas arbitrarias son teoremas del sistema lógico. Por ejemplo, la lógica proposicional es decidible, porque el método de la tabla de verdad puede utilizarse para 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ógicas en cualquier firma que incluya igualdad y al menos otro 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, las validez del cálculo de predicados monádicos con identidad son decidibles. Este sistema es lógica de primer orden restringida a aquellas firmas que no tienen símbolos de función y cuyos símbolos de relación distintos de la igualdad nunca toman más de un argumento.

Algunos sistemas lógicos no están adecuadamente representados por el conjunto de teoremas solo. (Por ejemplo, la lógica de Kleene no tiene teoremas en absoluto.) En tales casos, a menudo se utilizan definiciones alternativas de decidibilidad de un sistema lógico, que piden un método eficaz para determinar algo más general que la mera validez de fórmulas; por ejemplo, la validez de los consecuentes , 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 supone que están cerradas bajo la consecuencia lógica . La decidibilidad de una teoría se refiere a si existe un procedimiento efectivo que decide si la fórmula es miembro de la teoría o no, dada una fórmula arbitraria en la firma de la teoría. 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 la signatura de la teoría será una consecuencia lógica de la teoría y, por lo tanto, un miembro de ella. Toda teoría de primer orden recursivamente enumerable y completa es decidible. Una extensión de una teoría decidible puede no ser decidible. Por ejemplo, hay 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 tiene la propiedad de que toda extensión consistente es indecidible se dice que es 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 y, por lo tanto, toda teoría consistente que incluya o interprete la aritmética de Robinson también es (esencialmente) indecidible.

Los ejemplos de teorías de primer orden decidibles incluyen la teoría de campos 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 firma con sólo igualdad, establecido por Leopold Löwenheim en 1915.
• El conjunto de validez lógica de primer orden en una firma con igualdad y una función unaria, establecido por Ehrenfeucht en 1959.
• La teoría de primer orden de los números naturales en la signatura con igualdad y adición, también llamada aritmética de Presburger . La completitud fue establecida por Mojżesz Presburger en 1929.
• La teoría de primer orden de los números naturales en la signatura con igualdad y multiplicación, también llamada aritmética de Skolem .
• La teoría de primer orden de las álgebras de Boole , establecida por Alfred Tarski en 1940 (fundada en 1940 pero anunciada en 1949).
• La teoría de primer orden de campos algebraicamente cerrados de una característica dada , establecida por Tarski en 1949.
• La teoría de primer orden de campos ordenados realmente 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 (ver 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 (Monk 1976, p. 279): ^[2]

• El conjunto de validez lógica en cualquier firma de primer orden con igualdad y: un símbolo de relación 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 adición, multiplicación e igualdad, establecida por Tarski y Andrzej Mostowski en 1949.
• La teoría de primer orden de los números racionales con adición, multiplicación e igualdad, establecida por Julia Robinson en 1949.
• La teoría de primer orden de grupos , establecida por Alfred Tarski en 1953. ^[3] Cabe destacar que no solo la teoría general de grupos es indecidible, sino también varias teorías más específicas, por ejemplo (como la establecida por Mal'cev 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 campos 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 lo 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 esencialmente indecidible T 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 de 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, llega como positivo, si la fórmula está en la teoría; de lo contrario, puede que nunca llegue; de ​​lo contrario, llega como negativo. Un sistema lógico es semidecidible si existe un método bien definido para generar una secuencia de teoremas de manera que cada teorema eventualmente será generado. Esto es diferente de la decidibilidad porque en un sistema semidecidible puede no haber un procedimiento efectivo para verificar que una fórmula no es un teorema.

Toda teoría o sistema lógico decidible es semidecidible, pero en general la inversa no es cierta; 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, es porque no hay un método efectivo para determinar para una fórmula arbitraria A si A no está en V . De manera similar, el conjunto de consecuencias lógicas de cualquier conjunto recursivamente enumerable de axiomas de primer orden es semidecidible. Muchos de los ejemplos de teorías de primer orden indecidibles dados anteriormente son de esta forma.

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

Al igual que con el concepto de un conjunto decidible , la definición de una teoría decidible o un sistema lógico puede darse en términos de métodos efectivos o en términos de funciones computables . Estos generalmente se consideran equivalentes según la tesis de Church . De hecho, la prueba de que un sistema lógico o una teoría es indecidible utilizará la definición formal de computabilidad para mostrar que un conjunto apropiado no es un conjunto decidible, y luego invocará la tesis de Church para mostrar que la teoría o el sistema lógico no es decidible por ningún método efectivo (Enderton 2001, pp. 206 y siguientes ).

Algunos juegos han sido clasificados según su decidibilidad:

• El ajedrez es decidible. ^{[5] [6]} Lo mismo se aplica a todos los demás juegos finitos de dos jugadores con información perfecta.
• El mate en n en ajedrez infinito (con limitaciones en las reglas y piezas del juego) es decidible. ^{[7] [8]} Sin embargo, hay posiciones (con un número finito de piezas) que son victorias forzadas, pero no mate en n para ningún número finito de n . ^[9]
• Algunos juegos de equipo con información imperfecta en un tablero finito (pero con tiempo ilimitado) son indecidibles. ^[10]

• Problema de resolución de problemas
• Cuantificación existencial

• Barwise, Jon (1982), "Introducción a la lógica de primer orden", en Barwise, Jon (ed.), Handbook of Mathematical Logic , Estudios de lógica y fundamentos de las matemáticas, Ámsterdam: Holanda Septentrional, ISBN 978-0-444-86388-1
• Cantone, D.; Omodeo, EG; Policriti, A. (2013) [2001], Teoría de conjuntos para computación. De los procedimientos de decisión a la programación lógica con conjuntos, Monografías en Ciencias de la Computación, Springer, ISBN 9781475734522
• Chagrov, Alexander; Zakharyaschev, Michael (1997), Lógica modal , Oxford Logic Guides, vol. 35, Oxford University Press, ISBN 978-0-19-853779-3, Sr.  1464942
• Davis, Martin (2013) [1958], Computabilidad e insolubilidad, Dover, ISBN 9780486151069
• Enderton, Herbert (2001), Una introducción matemática a la lógica (2.ª ed.), Academic Press , ISBN 978-0-12-238452-3
• Keisler, HJ (1982), "Fundamentos de la teoría de modelos", en Barwise, Jon (ed.), Handbook of Mathematical Logic , Estudios de lógica y fundamentos de las matemáticas, Ámsterdam: Holanda Septentrional, ISBN 978-0-444-86388-1
• Monk, J. Donald (2012) [1976], Lógica matemática , Springer-Verlag , ISBN 9781468494525