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.
Referencias
Alonzo Church, "An unsolvable problem of elementary number theory", American Journal of Mathematics, 58 (1936), pp 345 - 363
Alonzo Church, "A note on the Entscheidungsproblem", Journal of Symbolic Logic, 1 (1936), pp 40 - 41.
Alan Turing, "On computable numbers, with an application to the Entscheidungsproblem", Proceedings of the London Mathematical Society, Series 2, 42 (1936), pp 230 - 265. Versión en-línea. Errata appeared in Series 2, 43 (1937), pp 544 - 546.
Datos:Q11030584
Septiembre 21, 2021
entscheidungsproblem, ciencias, computación, matemáticas, español, problema, decisión, reto, lógica, simbólica, encontrar, algoritmo, general, decidiese, fórmula, cálculo, primer, orden, teorema, 1936, manera, independiente, alonzo, church, alan, turing, demos. En 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 Referencias EditarAlonzo Church An unsolvable problem of elementary number theory American Journal of Mathematics 58 1936 pp 345 363 Alonzo Church A note on the Entscheidungsproblem Journal of Symbolic Logic 1 1936 pp 40 41 Alan Turing On computable numbers with an application to the Entscheidungsproblem Proceedings of the London Mathematical Society Series 2 42 1936 pp 230 265 Version en linea Errata appeared in Series 2 43 1937 pp 544 546 Datos Q11030584Obtenido de https es wikipedia org w index php title Entscheidungsproblem amp oldid 128447294, wikipedia, wiki, leyendo, leer, libro, biblioteca,
