Entscheidungsproblem

En ciències de la computació i matemàtiques, el Entscheidungsproblem (en espanyol: problema de decisió) va ser el repte en llògica simbòlica de trobar un algoritme general que decidira si una fòrmula del càlcul de primer orde és un teorema. En 1936, de manera independent, Alonzo Church i Alan Turing varen demostrar abdós que és impossible escriure tal algoritme. Com a conseqüència, és també impossible decidir en un algoritme si certes frases concretes de l'aritmètica són certes o falses.

La pregunta es remonta a Gottfried Leibniz, qui en el XVII, despuix de construir exitosamente una màquina mecànica de càlcul, somiava en construir una màquina que poguera manipular símbols per a determinar si una frase en matemàtiques és un teorema. Lo primer que seria necessari és un llenguage formal clar i precís, i molt del seu treball posterior es va dirigir cap a eixe objectiu. En 1928, David Hilbert i Wilhelm Ackermann varen propondre la pregunta en la seua formulació anteriorment mencionada.

Una fòrmula llògica de primer orde és cridada universalment vàlida o llògicament vàlida si es deduïx dels axioma del càlcul de primer orde. El teorema de completitud de Gödel establix que una fòrmula llògica és universalment vàlida en este sentit si i només si és certa en tota interpretació de la fòrmula en un model.

Abans de poder respondre a esta pregunta, va caldre definir formalment la noció de algoritme. Açò va ser realisat per Alonzo Church en 1936 en el concepte de "calculabilidad efectiva" basada en el seu càlcul lambda i per Alan Turing basant-se en la màquina de Turing. Els dos enfocaments són equivalents, en el sentit en que es poden resoldre exactament els mateixos problemes en abdós enfocaments.

La resposta negativa al Entscheidungsproblem va ser donada per Alonzo Church en 1936 i independentment, molt poc temps despuix per Alan Turing, també en 1936. Church va demostrar que no existix algoritme (definit segons les funcions recursivas) que decidixca per a dos expressions del càlcul lambda si són equivalents o no. Church para açò es va basar en treball previ de Stephen Kleene. Per una atra part, Turing va reduir este problema al problema de la parada per a les màquines de Turing. Generalment es considera que la prova de Turing ha tingut més influencia que la de Church. Abdós treballs es varen vore influïts per treballs anteriors de Kurt Gödel sobre el teorema de incompletitud, especialment pel método d'assignar números a les fòrmules llògiques per a poder reduir la llògica a l'aritmètica.

L'argument de Turing és com seguix: Suponga's que es té un algoritme general de decisió per a la llògica de primer orde. Es pot traduir la pregunta sobre si una màquina de Turing termina com una fòrmula de primer orde, que llavors podria ser somesa a l'algoritme de decisió. Pero Turing ya havia demostrat que no existix algoritme general que puga decidir si una màquina de Turing es para.

És important notar que si es restringix el problema a una teoria de primer orde específica en constants, predicats constants i axioma, és possible que existixca un algoritme de decisió per a la teoria. Alguns eixemples de teories decidibles són: l'aritmètica de Presburger i els sistemes estàtics de tipos dels Llenguages de programació.

No obstant, la teoria general de primer orde per als número natural coneguda com l'aritmètica de Peano no pot ser decidida en eixe tipo d'algoritme. Açò es deduïx de l'argument de Turing resumit més dalt.

Bibliografia

• 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, Séries 2, 42 (1936), pp 230 - 265. Versió en llínea. Errata appeared in Séries 2, 43 (1937), pp 544-546.