Avgörbarhetsproblemet

Inom matematik och datavetenskap är Avgörbarhetsproblemet eller Entscheidungsproblemet (av tyskans Entscheidung 'beslut') en fråga som ursprungligen formulerades av David Hilbert 1928:

” Finns det en algoritm som tar en given utsaga inom första ordningens logik som indata (möjligen med ytterligare ett begränsat antal axiom förutom de vanliga axiomen i första ordningens logik) och svarar "Ja" eller "Nej" på frågan om den är sann för alla möjliga giltiga värden av variablerna i utsagan? „

Enligt Gödels fullständighetssats för första ordningens logik är en utsaga universellt giltig om och endast om den kan härledas från dess axiom, så avgörbarhetsproblemet kan också ses som frågan om huruvida en utsaga är bevisbar utifrån axiomen eller inte.

År 1936 respektive 1937 publicerade Alonzo Church och Alan Turing oberoende av varandra artiklar som visar att en allmän lösning på avgörbarhetsproblemet inte existerar.[1] Dessa resultat är nu känd som Churchs teorem och Church-Turings hypotes. Avgörbarhetsproblemet har beröring med Hilberts tionde problem angående algoritmer för lösningar till Diofantiska ekvationer. Avsaknaden av någon sådan algoritm, fastställt av Yuri Matiyasevich 1970, innebär också ett negativt svar på avgörbarhetsproblemet.

Problemets bakgrund

Ursprunget till Entscheidungsproblemet går tillbaka till Gottfried Leibniz, som efter att på 1600-talet ha konstruerat en fungerande mekanisk räknemaskin drömde om att bygga en maskin som kunde manipulera symboler för att bestämma sanningsvärden för matematiska uttalanden.[2] Han ansåg att steg i den riktningen måste vara att konstruera ett mer formellt språk och mycket av hans följande arbete inriktades mot detta mål.

1928 formulerade David Hilbert och Wilhelm Ackermann frågan på det sätt som beskrivs ovan. Som en fortsättning på den problemlista" som David Hilbert lade fram vid en konferens i Paris år 1900, ställde han 1928 ytterligare tre frågor, varav den tredje blivit känd som "Hilberts Entscheidungsproblem".[3] Så sent som 1930 trodde Hilbert fortfarande att sådana problem inte kunde vara oavgörbara.[4]

Negativt svar

Innan frågan kunde besvaras måste begreppet "algoritm" ges en formell definition. Detta gjorde Alonzo Church år 1936 med begreppet "effektiv kalkylerbarhet" baserat på sin lambdakalkyl och Alan Turing samma år med begreppet Turingmaskin. Turing insåg snabbt att detta var likvärdiga modeller för beräkningsbarhet.

Church visade 1935–1936 att det inte finns någon beräkningsbar funktion som visar om två uttryck inom lambdakalkylen är ekvivalenta eller inte.

Turing likställde 1936–1937 det s.k. stopproblemet för Turingmaskiner med avgörbarhetsproblemet. Hans argument var som följer: Antag att vi har en generell avgörbarhetsalgoritm för utsagor i första ordningens logik. Frågan om huruvida en viss Turingmaskin stoppar inom ett ändligt antal programsteg eller inte kan formuleras som en första ordningens utsaga som denna algoritm då skulle kunna appliceras på. Men Turing hade tidigare visat att ingen allmän algoritm kan avgöra om en Turingmaskin stoppar eller ej och därmed inte heller någon sådan algoritm för första ordningens logik.

Bådas arbeten var starkt påverkade av Kurt Gödel och dennes ofullständighetssats, särskilt hans metod för tilldelning av tal (s.k. Gödeltal) till logiska formler och därigenom likställa logiska utsagor med aritmetiska tal.

Några första ordningens teorier är dock algoritmiskt avgörbara. Exempel på detta är Presburgeraritmetik, reella slutna algebraiska fält och statiska typsystem som förekommer i (de flesta) programmeringsspråk.

Referenser

Noter

  1. ^ Churchs rapport presenterades för American Mathematical Society den 19 April 1935 och publicerades 15 April 1936. Turing, som hade gjort stora framsteg med att dokumentera sitt eget resultat skyndade sig då att färdigställa det och få det publicerat. Det mottogs av Proceedings of the London Mathematical Society den 28 Maj 1936, och publicerades i januari 1937, serie 2, volym 42 (1936-1937); Turing gjorde sedan tillägg och korrigeringar i volym 43 (1938) s. 544-546. Se Davis 1965:116.
  2. ^ Davis 2000: s. 3-20
  3. ^ Hodges s. 91
  4. ^ Hodges s. 92, som citerar Hilbert

Allmänna källor

  • Alonzo Church, "An unsolvable problem of elementary number theory", American Journal of Mathematics, 58 (1936), s. 345–363
  • Alonzo Church, "A note on the Entscheidungsproblem", Journal of Symbolic Logic, 1 (1936), s. 40–41.
  • Martin Davis, 2000, Engines of Logic, W.W. Norton & Company, London, ISBN 0-393-32229-7 pocketbok.
  • Alan Turing, "On computable numbers, with an application to the Entscheidungsproblem", Proceedings of the London Mathematical Society, Serie 2, 42 (1937), s. 230–265. Online-versioner: från Oxford Journals webbplats, från Turing Digital Archive, från abelard.org. Rättningar infördes i Serie 2, 43 (1937), s. 544–546.
  • Martin Davis, "The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions", Raven Press, New York, 1965. Turings artikel är nr 3 i denna volym. Artkilar av Gödel, Church, Rosser, Kleen och Post ingår.
  • Andrew Hodges, Alan Turing: The Enigma, Simon and Schuster, New York, 1983. Alan M. Turings biografi. Jfr kapitel "The Spirit of Truth" för bakgrunden till, och en diskussion om hans bevis.
  • Stephen Toulmin, "Fall of a Genius", en bokrecension av "Alan Turing: The Enigma by Andrew Hodges", i The New York Review of Books, 19 januari 1984, s. 3 ff.
  • Alfred North Whitehead och Bertrand Russell, Principia Mathematica to *56, Cambridge University Press, 1962. Re: the problem of paradoxes; Författarna diskuterar problemet med en mängd som inte är objekt till någon av sina "determining functions", speciellt "Introduction, kap. 1 s. 24 "...difficulties which arise in formal logic", och kap. 2.I. "The Vicious-Circle Principle" s. 37 ff, och kap. 2.VIII. "The Contradictions" s. 60 ff.