Entscheidungsproblem

En ciencias de la computación y matemáticas, el Entscheidungsproblem (en español: problema de decisión) fue el reto en lógica simbólica de encontrar un algoritmo general que decidiese si una fórmula del cálculo de primer orden es un teorema. En 1936, de manera independiente, Alonzo Church y Alan Turing demostraron ambos que es imposible escribir tal algoritmo. Como consecuencia, es también imposible decidir con un algoritmo si ciertas frases concretas de la aritmética son ciertas o falsas.

La pregunta se remonta a Gottfried Leibniz, quien en el siglo XVII, después de construir exitosamente una máquina mecánica de cálculo, soñaba con construir una máquina que pudiera manipular símbolos para determinar si una frase en matemáticas es un teorema. Lo primero que sería necesario es un lenguaje formal claro y preciso, y mucho de su trabajo posterior se dirigió hacia ese objetivo. En 1928, David Hilbert y Wilhelm Ackermann propusieron la pregunta en su formulación anteriormente mencionada.

Una fórmula lógica de primer orden es llamada universalmente válida o lógicamente válida si se deduce de los axiomas del cálculo de primer orden. El teorema de completitud de Gödel establece que una fórmula lógica es universalmente válida en este sentido si y sólo si es cierta en toda interpretación de la fórmula en un modelo.

Antes de poder responder a esta pregunta, hubo que definir formalmente la noción de algoritmo. Esto fue realizado por Alonzo Church en 1936 con el concepto de "calculabilidad efectiva" basada en su cálculo lambda y por Alan Turing basándose en la máquina de Turing. Los dos enfoques son equivalentes, en el sentido en que se pueden resolver exactamente los mismos problemas con ambos enfoques.

La respuesta negativa al Entscheidungsproblem fue dada por Alonzo Church en 1936 e independientemente, muy poco tiempo después por Alan Turing, también en 1936. Church demostró que no existe algoritmo (definido según las funciones recursivas) que decida para dos expresiones del cálculo lambda si son equivalentes o no. Church para esto se basó en trabajo previo de Stephen Kleene. Por otra parte, Turing redujo este problema al problema de la parada para las máquinas de Turing. Generalmente se considera que la prueba de Turing ha tenido más influencia que la de Church. Ambos trabajos se vieron influidos por trabajos anteriores de Kurt Gödel sobre el teorema de incompletitud, especialmente por el método de asignar números a las fórmulas lógicas para poder reducir la lógica a la aritmética.

El argumento de Turing es como sigue: Supóngase que se tiene un algoritmo general de decisión para la lógica de primer orden. Se puede traducir la pregunta sobre si una máquina de Turing termina como una fórmula de primer orden, que entonces podría ser sometida al algoritmo de decisión. Pero Turing ya había demostrado que no existe algoritmo general que pueda decidir si una máquina de Turing se para.

Es importante notar que si se restringe el problema a una teoría de primer orden específica con constantes, predicados constantes y axiomas, es posible que exista un algoritmo de decisión para la teoría. Algunos ejemplos de teorías decidibles son: la aritmética de Presburger y los sistemas estáticos de tipos de los Lenguajes de programación.

Sin embargo, la teoría general de primer orden para los números naturales conocida como la aritmética de Peano no puede ser decidida con ese tipo de algoritmo. Esto se deduce del argumento de Turing resumido más arriba.