Problema de decisión (Entscheidungsproblem) en lógica y computación

Enunciado formal y alcance

De forma informal, el Entscheidungsproblem pide un algoritmo —un método efectivo y mecánico— que tome como entrada la descripción de un sistema formal y una fórmula en ese sistema, y devuelva siempre «verdadero» (la fórmula es demostrable o válida) o «falso» (no lo es). El programa de Hilbert y sus contemporáneos buscaba esos métodos de decisión para sistemas lógicos y para la aritmética. La formulación depende de las nociones de lenguaje formal, sintaxis y una noción efectiva de computación o algoritmo.

Desarrollo histórico

David Hilbert y otros plantearon preguntas metamatemáticas precisas en la década de 1920. El trabajo de varios lógicos durante la década de 1930 aclaró los límites de lo que puede decidirse mecánicamente. Alonzo Church utilizó el cálculo lambda y la noción de calculabilidad efectiva para mostrar que no existe un procedimiento general de decisión para la lógica de primer orden en su aplicación a la aritmética. De manera independiente, Alan Turing introdujo un modelo abstracto de máquina para captar la computación y demostró un resultado negativo equivalente al formular un problema indecidible sobre el comportamiento de las máquinas.

Ideas centrales de las demostraciones

Ambos enfoques se basaron en reducciones a partir de una cuestión ya conocida como indecidible. Church recurrió al poder expresivo de las funciones definibles por lambda para codificar la validez lógica; Turing formuló el problema de la parada para sus máquinas y mostró que no tiene solución algorítmica. Los dos resultados son compatibles porque sus nociones formales de computación coinciden para las funciones efectivamente calculables. Una conexión relacionada es que la indecidibilidad de enunciados sobre los números naturales (aritmética) se sigue de estas construcciones.

Consecuencias e importancia

La resolución negativa del Entscheidungsproblem tiene varias implicaciones duraderas:

• Establece límites intrínsecos de la formalización: algunas afirmaciones matemáticas verdaderas no pueden decidirse mediante un solo algoritmo.
• Llevó directamente al desarrollo de la teoría de la computabilidad y la teoría de la complejidad, al aclarar qué problemas son resolubles en principio.
• Influyó en el estudio de los sistemas formales, la demostración automática de teoremas y la clasificación de teorías decidibles e indecidibles.

Distinciones y ejemplos relacionados

No todos los sistemas formales son indecidibles. Algunas teorías restringidas admiten procedimientos de decisión (por ejemplo, la aritmética de Presburger es decidible, mientras que la aritmética de Peano no lo es). El Entscheidungsproblem se refiere a la existencia de un solucionador universal para clases enteras de enunciados; fragmentos o lenguajes concretos pueden ser decidibles o indecidibles según su poder expresivo. Para ampliar la lectura sobre los artículos históricos y los tratamientos técnicos, consulte materiales sobre lenguajes formales y introducciones a la lógica de las matemáticas, o biografías y exposiciones sobre Turing y Church.

Para resúmenes breves y tratamientos modernos, consulte textos de revisión y recursos en línea fiables que expliquen el problema de la parada, las reducciones y los límites de la decidibilidad algorítmica; estas fuentes suelen ofrecer ejemplos resueltos y demostraciones esquemáticas de por qué no puede existir un algoritmo universal de decisión. Véanse también las discusiones históricas sobre el programa de Hilbert y sobre cómo la solución negativa transformó las expectativas acerca de los fundamentos formales de la matemática.