Unbeweisbares Verhalten einer Turingmaschine

Ja, Ihr Verständnis ist grundsätzlich richtig - dies ist (soweit wir wissen) ein mögliches Ergebnis. Das Problem ist, dass es Modelle von ZFC geben kann, in denen es "nicht standardmäßige" natürliche Zahlen gibt. Diese nicht standardmäßigen Zahlen entsprechen nicht standardmäßigen Instanzen von SAT, die der Algorithmus$\alpha$kann möglicherweise nicht gelöst werden, obwohl es alle tatsächlichen Instanzen von SAT löst.

Es stellt sich heraus, dass eine vom Standard abweichende Laufzeit kein Problem darstellt - wenn$\alpha$läuft in polynomieller Zeit$p$, betrachten Sie den Algorithmus$\alpha'$was durchführt$\alpha$für$p$- viele Schritte, und dann - wenn es noch nicht angehalten hat - anhält und 1 ausgibt (sagen wir). Dann$\alpha'$löst alle tatsächlichen Instanzen von SAT und sogar nicht standardmäßig$\alpha'$läuft in polynomieller Zeit. Es geht also wirklich um nicht standardmäßige Instanzen von SAT.

Dies ist analog zu Gödels Unvollständigkeitssatz : obwohl es keine tatsächliche Codierung natürlicher Zahlen gibt, für die ein Beweis vorliegt$0=1$Aus den ZFC-Axiomen (wir hoffen: P) wird es ein Modell von ZFC geben, das einige nicht standardmäßige natürliche Zahlen enthält$n$was (das Modell denkt) kodiert einen Beweis von$0=1$aus$ZFC$- das heißt, ein "nicht standardmäßiger Beweis".

Es kann hilfreich sein, verschiedene Möglichkeiten zu unterscheiden$P = NP$könnte wahr sein, aber nicht beweisbar wahr. Damit$P = NP$, muss es eine Turing-Maschine geben$T$das löst SAT in polynomieller Zeit. Aber:

1. Es könnte unmöglich sein zu beweisen, dass es immer anhält.
2. Es könnte möglich sein zu beweisen, dass es immer anhält, aber unmöglich zu beweisen, dass es immer ein korrektes Ergebnis liefert.
3. Es könnte möglich sein zu beweisen, dass es immer anhält, aber unmöglich zu beweisen, dass es in polynomieller Zeit anhält.

Das sollte nicht so seltsam sein. Viele ungelöste mathematische Probleme lassen sich in Form von Fragen zu einer Turingmaschine formulieren. Beispielsweise ist die Collatz-Vermutung genau dann wahr, wenn eine bestimmte Turing-Maschine immer anhält.

Es gibt eine Möglichkeit, dass die Lösung nicht konstruktiv ist: Sie haben zB ein Universum, in dem keine Turing-Maschine SAT in Polynomzeit löst, und Sie haben ein anderes Universum, in dem es unmöglich ist, dass alle Turing-Maschinen SAT nicht in Polynomzeit lösen. Letzteres ist konstruktiv nicht gleichbedeutend mit der Suche nach einer Turing-Maschine, die SAT in Polynomialzeit löst; Du hast noch nie einen gefunden.

Dies kann ein wenig umformuliert werden. Der Satz von Ladner besagt, dass wenn$\mathrm{P}\neq \mathrm{NP}$dann gibt es eine NP-Zwischensprache (eine Sprache heißt NP-Zwischensprache, wenn sie in$\mathrm{NP}\setminus \mathrm{P}$und ist nicht NP-vollständig). Daher ist es theoretisch möglich, das Unabhängigkeitsergebnis wie folgt zu beweisen: Konstruieren Sie ein Universum, in dem es keine NP-Zwischensprache gibt (so$\mathrm{P}=\mathrm{NP}$) und eine andere konstruieren, in der es unmöglich ist, dass alle Sprachen nicht NP-intermediär sind (so$\mathrm{P}\neq \mathrm{NP}$). Auch hier würde keine Turing-Maschine gefunden werden.

(In Noahs Antwort scheint es, dass, wenn es so etwas gibt$\alpha$, der Algorithmus, der alle tatsächlichen Instanzen von SAT in polynomieller Zeit löst, dann sollten wir akzeptieren$\mathrm{P}=\mathrm{NP}$als eine von ZFC unabhängige Wahrheit . Ich bin mir nicht sicher, ob irgendein Algorithmus gegeben ist$\alpha$, der Ausdruck "$\alpha$löst SAT in polynomieller Zeit" ist$\Pi_1$(in PA/ZFC) oder nicht. Wenn ja, dann ist ein bestimmter Algorithmus gegeben$\alpha$, wann immer wir das wissen$\phi:=$"$\alpha$löst SAT in polynomieller Zeit" unabhängig von PA/ZFC ist, dann können wir das tatsächlich schlussfolgern$\phi$ist wahr , da sich PA/ZFC als wahr erweist$\Sigma_1$-Sätze, und wenn$\neg\phi$wahr wären, würde PA/ZFC es beweisen.)