[DE] Betrachtung des Widerspruchsbeweis des speziellen Halteproblems nach Vossen und Witt
Oft wird der Nachweis, dass das Halteproblem nicht entscheidbar ist, in der Fachliteratur (Schöning [📖Sch08, 119 f.], Asteroth und Baier [📖BA02, 106 f.], Sipser [📖Sip12, 216 f.]) mithilfe einer Turingmaschine und einem Widerspruchsbeweis gezeigt, in etwa:
Angenommen,
ist entscheidbar.
Sei ist die Turingmaschine, die entscheidet.
Sei die Codierung1 einer Turingmaschine, die wie folgt arbeitet:
- simuliert das Verhalten von bei der Eingabe :
- stoppt, wenn die Eingabe verwirft ()
- stoppt nicht, wenn die Eingabe akzeptiert ()
Damit folgt: stoppt bei Eingabe verwirft stoppt nicht
Widerspruch!
Bei Vossen und Witt wird der Beweis anhand unentscheidbarer Mengen gezeigt - hierzu wird in dem Abschnitt über Berechenbarkeit die Abzählbarkeit von Turingmaschinen und analog dazu die Standardnummerierung von 2 als theoretischer Unterbau festgelegt, um darauf aufbauend den Nachweis der Semi-Entscheidbarkeit und Unentscheidbarkeit zu führen. Im Folgenden findet sich die Beweisführung nach Vossen und Witt [📖VW16, 360 ff.] mit ergänzenden Kommentaren.
Die Standardnummerierung ist festgelegt als:
- : Die Menge aller Turingmaschinen (ein repräsentiert die Gödelnummer einer Turingmaschine), wobei die Menge aller normierten Turingmaschinen ist. Die Abbildung ist definiert durch bildet also auf eine natürliche Zahl eine Turingmaschine ab.
- : Die Menge aller berechenbaren Funktionen.
- ist eine Abzählung aller berechenbaren Funktionen. ist festgelegt durch Die berechenbare Funktion wird also durch die -te Turingmaschine berechnet.
Die Standardnummerierung ist im Folgenden die Grundlage für die Formulierung von Entscheidbarkeitsproblemen bei Mengen.