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ó...