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]
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 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:
