Unentscheidbarkeit der Arithmetik/Registermaschine/Fakt/Beweis

Aus Wikiversity
Zur Navigation springen Zur Suche springen
Beweis

Nach Fakt gibt es zu jedem Programm (mit Befehlen und Registern) einen arithmetischen Ausdruck in freien Variablen , der bei der Belegung mit genau dann wahr ist, wenn das Programm, angesetzt auf , schließlich mit der Konfiguration anhält. Der Ausdruck

besagt daher, dass das Programm bei Nulleingabe mit der Registerbelegung anhält und der Ausdruck (ohne freie Variablen)

besagt, dass das Programm überhaupt anhält. Es gilt also

genau dann, wenn bei Nulleingabe anhält. Man beachte, dass die Abbildung, die einem jeden Programm dieses zuordnet, effektiv durch eine Registermaschine durchführbar ist.

Wenn es ein Entscheidungsverfahren für arithmetische Sätze geben würde, so könnte man insbesondere auch die Richtigkeit von entscheiden. Doch dann würde es ein Entscheidungsverfahren für das Halteproblem im Widerspruch zu Fakt geben.

Zur bewiesenen Aussage