Hab auch nur wenig Ahnung von der ganzen Geschichte, habe jetzt aber bisschen rumgeklickt (hauptsächlich englische Wikipedia und
Math Stackexchange und das von mir schon erwähnte Logicomix), und versuche mich mal an einer Formulierung, ohne Garantie auf Richtigkeit.
Hier mal eine Formuilerung des Entscheidungsproblem (
Quelle):
Entscheidungsproblem schrieb:Gibt es ein Verfahren, das für jede ausreichend formalisierte Aussage der Mathematik entscheidet, ob diese wahr oder falsch ist?
Das ist alles sehr unpräzise formuliert, was ist beispielsweise mit
ausreichend formalisierte Aussage gemeint? Googlet man ein bisschen, dann steht praktisch überall dass sich das Entscheidungsproblem aus Aussagen in der "First-Order Logic" (FOL) (dt. Prädikatenlogik erster Stufe) bezieht.
Hier mal eine mathematische Aussage über Natürliche Zahlen:
Für jede natürliche Zahl x existiert eine natürliche Zahl y die grösser ist als x.
Formuliert in First-Order Logic sieht das so aus (∀ steht "für alle" und ∃ für "es gibt"):
Zitat:∀ x ∃ y : y > x
Das ist eine mathematische Aussage, von der man jetzt beweisen könnte, dass sie wahr ist (in dem man beispielsweise zeigt, dass jeder Natürliche Zahl einen Nachfolger hat, die grösser ist als sie selber).
Es gibt auch noch "Second-Order Logic" oder "Prädikatenlogik zweiter Stufe" und andere Logiksysteme, die ich selber auch nicht wirklich kenne, in denen man aber Aussagen formulieren könnte.
Was für "First-Order Logic" beim Entscheidungsproblem jetzt wichtig scheint, ist der Vollständigkeitssatz von Gödel, der unter anderem besagt dass jede wahre Aussage in FOL auch beweisbar ist, was bei anderen Logiksystemen wohl nicht zwingend der Fall sein muss.
Um eine Aussage in FOL zu beweisen, benötigt man Axiome, also Aussagen die wir fix als wahr definieren, ohne sie beweisen zu müssen. Ein Beispiel für die Natürlichen Zahlen ist beispielsweise das Axiom: ∄ x : x + 1 = 0 ("es gibt
keine natürlich Zahl, die mit Eins addiert wieder Null ergibt")
Kleiner Exkurs: Nicht alle Axiome der Natürlichen Zahlen lassen sich in FOL ausdrücken. Das heisst, dass das Entscheidungsproblem nicht mal für nicht alle mathematischen Aussagen eine Rolle spielt.
Des Weiteren kann der Informatiker "ein Verfahren" mit "einen Algorithmus" ersetzen, und und damit nur Programme meinen, die auch garantiert irgendwann mal terminieren, also in endlicher Zeit fertig werden mit Rechnen. Denke die Definition von Algorithmus ist dir eh schon klar, sonst kann ich das noch ausführen.
Das Entscheidungsproblem etwas mathematischer formuliert würde also lauten:
Entscheidungsproblem schrieb:Gibt es einen Algorithmus, der für jede mögliche Aussage in First-Order Logic (und optional zusätzlich einer endlicher Anzahl von Axiomen in First-Order Logic) entscheidet, ob die Aussage wahr oder falsch ist.
Die Antwort auf diese Frage lautet
Nein. Es gibt keinen Algorithmus, der für
jede mögliche mathematische Aussage entscheiden kann, ob sie wahr oder falsch ist. Das haben Church und Turing unabhängig 1936/37 gezeigt.
Das freut die Gewerkschaft der Mathematiker, denn das Finden und Beweisen von gültigen mathematischen Aussagen kann damit bewiesenermassen nicht durch Computer erledigt werden.
Turing hat beispielsweise gezeigt, dass wenn es einen Algorithmus gäbe, der für jede FOL-Aussage entscheidet, ob sie wahr oder falsch ist, dass man mit Hilfe davon auch das Halteproblem lösen könnte. Das Halteproblem kann aber nicht gelöst werden. Also kann es keinen Algorithmus fürs Entscheidungsproblem geben.
Paar Links die ich verwendet habe:
http://www.infomutt.com/e/en/entscheidungsproblem.html
http://www.infomutt.com/f/fi/first_order...culus.html
http://www.karlin.mff.cuni.cz/~stovicek/...bility.pdf
http://en.wikipedia.org/wiki/Entscheidungsproblem
http://www.cl.cam.ac.uk/teaching/0910/Co...ture-1.pdf
