Entscheidungsproblem

In de wiskunde en informatica is het zogeheten Entscheidungsproblem (Duits: beslissingsprobleem) een uitdaging van David Hilbert in 1928. Het Entscheidungsproblem vraagt om een algoritme dat als invoer een uitspraak in een eerste-ordelogica (eventueel met een eindig aantal axioma's in plaats van de gebruikelijke axioma's van de eerste-ordelogica) krijgt en antwoordt met "ja" of "nee" al naargelang de uitspraak universeel geldig is of niet, dat wil zeggen, geldig in elke structuur die voldoet aan de axioma's. Vanwege de Volledigheidsstelling van Gödel is een uitspraak slechts dan universeel geldig als hij kan worden afgeleid uit de axioma's, zodat het Entscheidungsproblem ook kan worden gezien als de vraag naar een algoritme om te beslissen of een bepaalde uitspraak bewijsbaar is vanuit de axioma's met behulp van de regels van de logica.

In 1936 publiceerden Alonzo Church en Alan Turing onafhankelijk van elkaar artikelen die aantonen dat een algemene oplossing voor het Entscheidungsproblem niet mogelijk is, ervan uitgaande dat het intuïtieve begrip 'effectief berekenbaar' gedekt wordt door functies die berekenbaar zijn door een turingmachine. Deze veronderstelling is nu bekend als de Church-Turing-hypothese.

Geschiedenis

De oorsprong van het Entscheidungsproblem ligt bij Gottfried Leibniz, die in de zeventiende eeuw, na een succesvolle mechanische rekenmachine, ervan droomde een machine te bouwen die symbolen zou kunnen manipuleren om de waarheidswaarde van wiskundige uitspraken te bepalen. Hij besefte dat de eerste stap zou zijn om over een zuivere formele taal te kunnen beschikken, en veel van zijn latere werk was op dat doel gericht. In 1928 stelden David Hilbert en Wilhelm Ackermann de vraag in de hierboven geschetste vorm.

In het verlengde van zijn "programma" formuleerde Hilbert op een internationale conferentie in 1928 drie vragen, waarvan de derde bekend werd als Hilberts Entscheidungsproblem. Nog in 1930 geloofde hij niet dat er zoiets zou bestaan als een onoplosbaar probleem.

Negatief antwoord

Voordat de vraag kan worden beantwoord, moest het begrip "algoritme" eerst formeel gedefinieerd worden. Dit werd gedaan door Alonzo Church in 1936 met het begrip "effectieve berekenbaarheid" op basis van zijn λ-calculus en door Alan Turing in hetzelfde jaar met zijn concept turingmachine. Turing zag onmiddellijk in dat deze twee begrippen gelijkwaardige rekenmodellen zijn.

Het negatieve antwoord op het Entscheidungsproblem werd vervolgens door Church gegeven in 1935-1936 en onafhankelijk van hem kort daarna door Alan Turing in 1936. Church bewees dat er geen berekenbare functie bestaat die kan beslissen voor twee gegeven λ-calculus-expressies of ze gelijkwaardig zijn of niet. Hij leunde zwaar op eerder werk van Stephen Kleene. Turing bracht het stopprobleem voor turingmachines terug tot het Entscheidungsproblem. Het werk van beide auteurs werd sterk beïnvloed door Kurt Gödels eerdere werk voor zijn onvolledigheidsstelling, in het bijzonder door de methode van het toekennen van getallen (gödelnummers) aan logische formules om logica tot rekenkunde te herleiden.

Het Entscheidungsproblem is gerelateerd aan het tiende probleem van Hilbert, waarin wordt gevraagd naar een algoritme om te beslissen of diofantische vergelijkingen een oplossing hebben. Het niet-bestaan van een dergelijke algoritme, zoals vastgesteld door Joeri Matijasevitsj in 1970, impliceert ook een negatief antwoord op het Entscheidungsproblem.

Sommige eerste-ordetheorieën zijn algoritmisch beslisbaar. Voorbeelden hiervan zijn onder meer Presburger rekenkunde, reële gesloten lichamen en statische typesystemen van veel programmeertalen. De algemene eerste-ordetheorie van de natuurlijke getallen uitgedrukt in axioma's van Peano kan echter niet worden beslist met een dergelijk algoritme.