|
< Back | Wikipedia | Home | Dark Mode EntscheidungsproblemEn ciencias de la computacion y matematicas, el Entscheidungsproblem (en espanol: problema de decision) fue el reto en logica simbolica de encontrar un algoritmo general que decidiese si una formula del calculo 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 tambien imposible decidir con un algoritmo si ciertas frases concretas de la aritmetica son ciertas o falsas. La pregunta se remonta a Gottfried Leibniz, quien en el siglo XVII, despues de construir exitosamente una maquina mecanica de calculo, sonaba con construir una maquina que pudiera manipular simbolos para determinar si una frase en matematicas es un teorema. Lo primero que seria necesario es un lenguaje formal claro y preciso, y mucho de su trabajo posterior se dirigio hacia ese objetivo. En 1928, David Hilbert y Wilhelm Ackermann propusieron la pregunta en su formulacion anteriormente mencionada. Una formula logica de primer orden es llamada universalmente valida o logicamente valida si se deduce de los axiomas del calculo de primer orden. El teorema de completitud de Godel establece que una formula logica es universalmente valida en este sentido si y solo si es cierta en toda interpretacion de la formula en un modelo. Antes de poder responder a esta pregunta, hubo que definir formalmente la nocion de algoritmo. Esto fue realizado por Alonzo Church en 1936 con el concepto de "calculabilidad efectiva" basada en su calculo lambda y por Alan Turing basandose en la maquina 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 despues por Alan Turing, tambien en 1936. Church demostro que no existe algoritmo (definido segun las funciones recursivas) que decida para dos expresiones del calculo lambda si son equivalentes o no. Church para esto se baso en trabajo previo de Stephen Kleene. Por otra parte, Turing redujo este problema al problema de la parada para las maquinas de Turing. Generalmente se considera que la prueba de Turing ha tenido mas influencia que la de Church. Ambos trabajos se vieron influidos por trabajos anteriores de Kurt Godel sobre el teorema de incompletitud, especialmente por el metodo de asignar numeros a las formulas logicas para poder reducir la logica a la aritmetica. El argumento de Turing es como sigue: Supongase que se tiene un algoritmo general de decision para la logica de primer orden. Se puede traducir la pregunta sobre si una maquina de Turing termina como una formula de primer orden, que entonces podria ser sometida al algoritmo de decision. Pero Turing ya habia demostrado que no existe algoritmo general que pueda decidir si una maquina de Turing se para. Es importante notar que si se restringe el problema a una teoria de primer orden especifica con constantes, predicados constantes y axiomas, es posible que exista un algoritmo de decision para la teoria. Algunos ejemplos de teorias decidibles son: la aritmetica de Presburger y los sistemas estaticos de tipos de los Lenguajes de programacion. Sin embargo, la teoria general de primer orden para los numeros naturales conocida como la aritmetica de Peano no puede ser decidida con ese tipo de algoritmo. Esto se deduce del argumento de Turing resumido mas arriba.
Source: es.wikipedia.org |