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 la lógica 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 para ellos no puede existir 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 consecuencia semántica y sintáctica. En otros escenarios, 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 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 puede usarse 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 validaciones lógicas en cualquier firma que incluya la 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 una 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 por sí solos. (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 exigen un método eficaz para determinar algo más general que la mera validez de fórmulas; por ejemplo, validez de secuentes , o la relación de consecuencia {(Г, A ) | Г ⊧ A } de la lógica.