La decidibilidad algorítmica es una propiedad de una teoría formal de tener un algoritmo que determina mediante una fórmula dada si es derivable del conjunto de axiomas de la teoría dada o no. Se dice que una teoría es decidible si tal algoritmo existe, e indecidible en caso contrario. La cuestión de la deducibilidad en la teoría formal es un caso particular, pero al mismo tiempo el más importante de un problema más general de decidibilidad .
Los conceptos de algoritmo y sistema axiomático tienen una larga historia. Ambos se conocen desde la antigüedad . Baste recordar los postulados de la geometría de Euclides y el algoritmo para encontrar el máximo común divisor del mismo Euclides. A pesar de esto, no existió durante mucho tiempo una definición matemática clara del cálculo y especialmente del algoritmo. La peculiaridad del problema asociado con la definición formal de indecidibilidad fue que para mostrar que existe algún algoritmo, basta con encontrarlo y demostrarlo. Si no se encuentra el algoritmo, es posible que no exista, y entonces hay que probarlo rigurosamente. Y para esto necesitas saber exactamente qué es un algoritmo.
Hilbert y su escuela lograron grandes avances en la formalización de estos conceptos a principios del siglo XX . Luego, primero, se formaron los conceptos de cálculo y derivación formal, y luego Hilbert, en su famoso programa de fundamentación de las matemáticas , fijó la ambiciosa meta de formalizar todas las matemáticas. El programa proporcionaba, entre otras cosas, la posibilidad de comprobar automáticamente cualquier fórmula matemática para la verdad. Basándose en el trabajo de Hilbert, Gödel describió por primera vez una clase de las llamadas funciones recursivas , con las que demostró sus famosos teoremas de incompletitud . Posteriormente, se introdujeron una serie de otros formalismos, como la máquina de Turing , λ-calculus , que resultó ser equivalente a funciones recursivas. Cada uno de estos ahora se considera el equivalente formal de la noción intuitiva de una función computable. Esta equivalencia es postulada por la tesis de Church .
Cuando se refinaron los conceptos de cálculo y algoritmo, siguieron una serie de resultados sobre la indecidibilidad de varias teorías. Uno de los primeros resultados de este tipo fue un teorema probado por Novikov sobre la insolubilidad del problema de las palabras en grupos . Las teorías decidibles se conocían mucho antes.
Intuitivamente, cuanto más compleja y expresiva sea la teoría, mayor será la posibilidad de que resulte indecidible. Por lo tanto, en términos generales, una "teoría indecidible" es una "teoría compleja".
El cálculo formal en el caso general debe definir el lenguaje , las reglas para construir términos y fórmulas , los axiomas y las reglas de inferencia. Así, para cada teorema T siempre es posible construir una cadena A 1 , A 2 , … , A n = T , donde cada fórmula A i es un axioma o puede deducirse de las fórmulas anteriores según una de las derivaciones normas. La resolubilidad significa que hay un algoritmo que para cada oración T bien formada en un tiempo finito da una respuesta inequívoca: sí, esta oración es derivable dentro del marco del cálculo o no, no es derivable.
Es obvio que la teoría contradictoria es decidible, ya que cualquier fórmula será derivable. Por otro lado, si un cálculo no tiene un conjunto recursivamente enumerable de axiomas, como la lógica de segundo orden , obviamente no puede ser decidible.
La decidibilidad es una propiedad muy fuerte y la mayoría de las teorías útiles y prácticas no la tienen. En relación con esto, se introdujo una noción más débil de semidecidibilidad . Semidecidible significa tener un algoritmo que siempre confirmará en un tiempo finito que la oración es verdadera si es verdadera, pero si no lo es, puede ejecutarse indefinidamente.
El requisito de semidecidibilidad es equivalente a poder enumerar eficientemente todos los teoremas de una teoría dada. En otras palabras, el conjunto de teoremas debe ser recursivamente enumerable . La mayoría de las teorías utilizadas en la práctica satisfacen este requisito.
Los procedimientos semipermisivos eficientes para la lógica de primer orden son de gran importancia práctica, ya que permiten probar (semi)automáticamente declaraciones formalizadas de una clase muy amplia. Un gran avance en esta área fue el descubrimiento de Robinson del método de resolución en 1965 .
En lógica matemática , se utilizan tradicionalmente dos conceptos de completitud: completitud propiamente dicha y completitud con respecto a alguna clase de interpretaciones (o estructuras). En el primer caso, una teoría es completa si cada oración en ella es verdadera o falsa. En el segundo caso, si cualquier oración que es verdadera bajo todas las interpretaciones de la clase dada es derivable.
Ambos conceptos están íntimamente relacionados con la decidibilidad. Por ejemplo, si el conjunto de axiomas de una teoría completa de primer orden es recursivamente enumerable, entonces es decidible. Esto se deriva del famoso teorema de Post , que establece que si un conjunto y su complemento son recursivamente enumerables, entonces también son decidibles . Intuitivamente, el argumento que muestra la verdad del enunciado anterior es el siguiente: si la teoría es completa y el conjunto de sus axiomas es recursivamente enumerable, entonces existen procedimientos semipermisivos para probar la verdad de cualquier enunciado, así como su negación. Si ejecuta ambos procedimientos en paralelo , entonces, dada la integridad de la teoría, uno de ellos debería detenerse algún día y dar una respuesta positiva.
Si la teoría es completa con respecto a alguna clase de interpretaciones, esto puede usarse para construir un procedimiento de decisión. Por ejemplo , la lógica proposicional es completa con respecto a la interpretación en tablas de verdad . Por tanto, la construcción de una tabla de verdad según esta fórmula será un ejemplo de algoritmo de resolución para lógica proposicional.