En lógica , un problema de decisión verdadero/falso es decidible si existe un método eficaz 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 se puede determinar efectivamente la pertenencia a su conjunto de fórmulas (o teoremas) lógicamente válidos . Una teoría (conjunto de oraciones cerradas bajo consecuencia lógica ) en un sistema lógico fijo es decidible si existe un método eficaz 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 para ellos ningún método eficaz para determinar la pertenencia (devolver una respuesta correcta después de un tiempo finito, aunque posiblemente muy largo en todos los casos).
Cada sistema lógico viene con 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 consecuencias semánticas y sintácticas. En otros entornos, como la lógica lineal , la relación de consecuencia sintáctica (demostrabilidad) se puede utilizar para definir los teoremas de un sistema.
Un sistema lógico es decidible si existe un método eficaz para determinar si las 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 se puede utilizar 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ógica 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 validezes 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 representados adecuadamente sólo por el conjunto de teoremas. (Por ejemplo, la lógica de Kleene no tiene ningún teorema). 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 simple validez de las fórmulas; por ejemplo, validez de secuentes 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 cerradas según una consecuencia lógica . La decidibilidad de una teoría se refiere a si existe un procedimiento eficaz que decida 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.
Hay varios resultados básicos sobre la decidibilidad de las teorías. Toda teoría inconsistente (no paraconsistente ) es decidible, ya que cada fórmula en la firma 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 completa y recursivamente 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) es 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 campos 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.
Ejemplos de teorías de primer orden decidibles incluyen la teoría de campos cerrados reales 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 del cuantificador , la integridad 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 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, llegue como positivo, si la fórmula está en la teoría; de lo contrario, es posible 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 tal que eventualmente se genere cada teorema. Esto es diferente 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 lo contrario no es cierto; Una teoría es decidible si y sólo 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 eficaz 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 capacidad de decisión no debe confundirse con la integridad . Por ejemplo, la teoría de campos 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, debido a una ambigüedad terminológica, el término "enunciado indecidible" se utiliza a veces como sinónimo de enunciado independiente .
Al igual que con el concepto de conjunto decidible , la definición de una teoría o sistema lógico decidible 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 o teoría lógico 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 demostrar que la teoría o el sistema lógico no es decidible por ningún sistema efectivo. método (Enderton 2001, págs. 206 y siguientes ).
Algunos juegos se han clasificado según su decidibilidad:
