Gibt es Programme, die niemals anhalten und keine unbeendigten Beweise haben?

Wie schwarze Löcher in der Informatik. Wir können nur wissen, dass sie existieren, aber wenn wir einen von ihnen haben, werden wir nie wissen, dass es einer von ihnen ist.

Es gibt in der Tat Programme wie dieses. Um dies zu beweisen, nehmen wir im Gegenteil an, dass es für jede Maschine, die nicht anhält, einen Beweis gibt, dass sie nicht anhält.

Diese Beweise sind Zeichenfolgen endlicher Länge, sodass wir für einige ganze Zahlen s alle Beweise mit einer Länge von weniger als auflisten können .$s$$s$

Wir können dies dann verwenden, um das Halteproblem wie folgt zu lösen: Wenn eine Turing-Maschine und eine Eingabe x gegeben sind , verwenden wir den folgenden Algorithmus:$M$$x$

s := 0
while (True)
    test if machine M halts on input x in s steps
    look at all proofs of length s and see if they prove M doesn't halt on input x
    set s := s + 1

Wenn bei Eingabe x anhält , hält es in einer endlichen Anzahl von Schritten s an , sodass unser Algorithmus endet.$M$$x$$s$

Wenn bei Eingabe x nicht anhält , gibt es nach unserer Annahme einige Beweislängen s, in denen es einen Beweis gibt, dass M nicht anhält. In diesem Fall wird unser Algorithmus immer beendet.$M$$x$$s$$M$

Wir haben also einen Algorithmus, der über das Problem des Anhaltens entscheidet und der immer endet. Wir wissen jedoch, dass dies nicht existieren kann, und daher muss unsere Annahme, dass es immer einen Beweis für die Unaufhaltsamkeit gibt, falsch sein.

Für ein etwas konkreteres Beispiel nehmen wir an, dass die Theorie, die wir für unsere Beweise verwenden, die folgenden (durchaus vernünftigen, IMO) Merkmale aufweist:

1. Es ist konsequent ; das heißt, es kann keinen Widerspruch beweisen.
2. Seine Axiome sind rekursiv aufzählbar.
3. Seine Beweise können als endliche Bitstrings niedergeschrieben werden.
4. Die Frage, ob eine gegebene Zeichenkette einen wohlgeformten und korrekten Beweis darin codiert, ist algorithmisch in endlicher Zeit entscheidbar.
5. Es ist expressiv genug, einen Beweis für Gödels zweiten Unvollständigkeitssatz zuzulassen , der besagt, dass er seine eigene Konsistenz nicht beweisen kann.

Mit diesen Annahmen wird das folgende Programm niemals anhalten, aber es kann nicht bewiesen werden (im Rahmen der Theorie, die wir verwenden), dass es nicht anhält:

let k := 0;
repeat:
    let k := k + 1;
    let s := binary expansion of k, excluding leading 1 bit;
while s does not encode a proof of a contradiction;
halt.

Das Schlüsseldetail ist hier die erste Annahme, nämlich dass die Theorie, die wir für unsere Beweise verwenden, konsistent ist. Natürlich müssen wir dies annehmen, damit unsere Beweise irgendetwas wert sind, aber Gödels zweiter Unvollständigkeitssatz besagt, dass wir dies für jede einigermaßen aussagekräftige und effektiv axiomatisierte Theorie nicht beweisen können (außer möglicherweise in einer anderen Theorie, deren Konsistenz wir dann haben annehmen müssen, etc. etc.).