Entscheidungsproblem

De Viquip??dia

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. Al 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 amb 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. Al 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 al 1936 amb el concepte de ???calculabilitat efectiva??? basada en el seu c??lcul lambda i per Alan Turing en base a la seva m??quina de Turing. Els dos enfocs s??n equivalents en el sentit que poden resoldre exactament els mateixos problemes amb ambd??s enfocs.

La resposta negativa al Entscheidungsproblem fou donada per Alonzo Church al 1936 i independentment, molt poc despr??s per Alan Turing, tamb?? al 1936. Church va demostrar que no existeix algorisme (definit en base a 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 altre 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 influits per els treballs anteriors de Kurt G??del sobre el teorema d'incompletitut, especialment per el 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.

[edita] 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.