Entscheidungsproblem

El Entscheidungsproblem (en català: problema de decisió) fou el repte en lògica simbòlica de trobar un algorisme que decidís si una fórmula de càlcul de primer ordre és un teorema. El 1936, de manera independent, Alonzo Church i Alan Turing demostraren que és impossible escriure tal algorisme. Com a conseqüència, és també impossible decidir amb un algorisme si una frase qualsevol de l'aritmètica és certa o falsa.

La pregunta es remunta a Gottfried Leibniz, qui en el segle xvii, després de construir amb èxit una màquina mecànica de càlcul, somiava construir una màquina que pogués manipular símbols per a determinar si una frase en matemàtiques és un teorema. El primer que seria necessari és un llenguatge formal clar i precís, i molt del seu treball posterior es dirigí cap aquest objectiu. El 1928, David Hilbert i Wilhelm Ackermann proposaren la pregunta en la seva formulació anteriorment mencionada.

Una fórmula lògica de primer ordre és anomenada universalment vàlida o lògicament vàlida si es dedueix dels axiomes del càlcul de primer ordre. El teorema de completitut de Gödel estableix que una fórmula lògica és universalment vàlida en aquest sentit si i només si és certa en tota la interpretació de la fórmula en un model.

Abans de poder respondre a aquesta pregunta, es va haver de definir formalment la noció d'algorisme. Això fou realitzat per Alonzo Church el 1936 amb el concepte de "calculabilitat efectiva" basada en el seu càlcul lambda i per Alan Turing basant-se en la seva màquina de Turing. Els dos enfocaments són equivalents en el sentit que poden resoldre exactament els mateixos problemes amb ambdós enfocaments.

La resposta negativa al Entscheidungsproblem fou donada per Alonzo Church el 1936 i independentment, molt poc després per Alan Turing, també el 1936. Church va demostrar que no existeix algorisme (definit basant-se en funcions recursives) que decideixi per dos expressions de càlcul lambda si són equivalents o no. Church per això es va basar en el trebal previ de Stephen Kleene. Per altra part, Turing va reduir aquest problema al problema de la parada per les màquines de Turing. Generalment es considera que la prova de Turing ha tingut més influència que la de Church. Ambdós treballs es veieren influïts pels treballs anteriors de Kurt Gödel sobre el teorema d'incompletitut, especialment pel mètode d'assignar nombres a les fórmules lògiques per a poder reduir la lògica a l'aritmètica.

L'argument de Turing és com segueix: Suposem que es té un algorisme general de decisió per la lògica de primer ordre. Es pot traduir la pregunta si una màquina de Turing acaba com una fórmula de primer ordre, que llavors podria ser sotmesa a l'algorisme de decisió. Però Turing ja havia demostrat que no existeix algorisme general que pugui decidir si una màquina de Turing es para.

És important notar que si es restringeix el problema a una teoria de primer ordre específica amb constants, predicats constants i axiomes, és possible que existeixin algorismes de decisions per la teoria. Alguns exemples de teories decidibles són: l'aritmètica de Presburger i els sistemes estàtics de tipus dels Llenguatges de programació.

En canvi, la teoria general de primer ordre per als nombres naturals coneguda com l'aritmètica de Peano no pot ser decidida amb aquest tipus d'algorisme. Això es dedueix de l'argument de Turing resumit més amunt.

Referències

• 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ó en-línia. Errata appeared in Series 2, 43 (1937), pp 544 – 546.