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 se puede determinar efectivamente la pertenencia a su conjunto de fórmulas (o teoremas) lógicamente válidas . 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 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 la consecuencia semántica y sintáctica. En otros entornos, como la lógica lineal , la relación de consecuencia sintáctica (probabilidad) 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ógicas en cualquier signatura que incluya igualdad y al menos otro predicado con dos o más argumentos no es decidible. [1] Los sistemas lógicos que amplían 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 a los de igualdad nunca toman más de un argumento.
Algunos sistemas lógicos no están adecuadamente representados por el conjunto de teoremas solos. (Por ejemplo, la lógica de Kleene no tiene teoremas en absoluto). En tales casos, a menudo se usan definiciones alternativas de decidibilidad de un sistema lógico, que solicitan un método efectivo para determinar algo más general que solo la validez de las fórmulas; por ejemplo, la validez de los secuentes , o la relación de consecuencia {(Г, A ) | Ã ⊧ A } de la lógica.