Warum behauptet Turing, dass eine vollständige und berechenbare Axiomatisierung der Arithmetik die Entscheidbarkeit der Logik erster Ordnung implizieren würde?

Ich lese also gerade den berühmten Aufsatz von Turing "On Computable Numbers, with an Application to the Entscheidungsproblem". Zu Beginn seines Beweises der Unentscheidbarkeit der Logik erster Ordnung (FOL) behauptet er Folgendes:

Es sollte vielleicht bemerkt werden, dass das, was ich beweisen werde, ganz anders ist als die bekannten Ergebnisse von Gödel. Gödel hat gezeigt, dass es (im Formalismus der Principia Mathematica) Sätze 𐌵 gibt, bei denen weder 𐌵 noch ¬𐌵 beweisbar sind. Als Konsequenz daraus wird gezeigt, dass innerhalb dieses Formalismus kein Konsistenzbeweis von Principia Mathematica (oder von K ) gegeben werden kann. Andererseits werde ich zeigen, dass es keine allgemeine Methode gibt, die sagt, ob eine gegebene Formel 𐌵 in K beweisbar ist , oder, was auf dasselbe hinausläuft, ob das System bestehend aus K mit ¬𐌵 als zusätzlichem Axiom konsistent ist .

Wobei K die von Hilbert und Ackermann gegebene Axiomatisierung von FOL ist. Außerdem behauptet er:

Wenn die Negation dessen, was Gödel gezeigt hat, bewiesen wurde, dh wenn für jedes 𐌵 entweder 𐌵 oder ¬𐌵 beweisbar ist, dann sollten wir eine sofortige Lösung des Entscheidungsproblems haben. Denn wir können eine Maschine 𐌺 erfinden , die nacheinander alle beweisbaren Formeln beweist. Früher oder später wird 𐌺 entweder 𐌵 oder ¬𐌵 erreichen . Wenn es 𐌵 erreicht , wissen wir, dass 𐌵 beweisbar ist. Wenn es ¬𐌵 erreicht, dann wissen wir , da K konsistent ist (Hilbert und Ackermann, S. 65), dass 𐌵 nicht beweisbar ist.

Aus erster Hand und ohne weitere Klärung seinerseits scheint er also zwei verschiedene Arten von formalen axiomatischen Systemen gleichzusetzen: diejenigen, die versuchen, den Begriff der Gültigkeit in der Logik zu mechanisieren, und diejenigen, die versuchen, den Begriff der Wahrheit in der Arithmetik zu mechanisieren .

Was er wahrscheinlich erreichen möchte, ist, dass es eine Möglichkeit gibt, die Vorstellung, dass 𐌵 ein beweisbarer Satz in K ist, in Arithmetik zu codieren , so dass, wenn die Arithmetik vollständig wäre, dieser Satz in Arithmetik bewiesen oder widerlegt werden könnte.

Irgendwelche Vorschläge, um zu verstehen, wovon er hier spricht?

Vielen Dank im Voraus :)

Ich glaube nicht, dass er irgendetwas gleichsetzt, er macht eine triviale Beobachtung, dass alle Theoreme in einem rekursiv axiomatisierten System algorithmisch generiert werden können. Wenn also das System auch vollständig ist, ergibt sich ein Entscheidungsverfahren zur Beweisbarkeit eines beliebigen Satzes. Denn wenn wir einfach alle Theoreme einzeln generieren, wird schließlich entweder 𐌵 oder ¬𐌵 generiert und die Prozedur wird garantiert beendet.
Axiomatische Systeme von FOL sind von anderer Natur als axiomatische Systeme für die Mathematik (als Postulate von FOL kodifiziert). Nehmen wir ein axiomatisches System der Arithmetik. In der Arithmetik ist jeder Ausdruck ohne freie Variablen entweder wahr oder falsch. Wenn es also ein vollständiges System gibt, wird schließlich jeder Ausdruck darin erscheinen (entweder bejaht oder verneint). Bei einer Axiomatisierung von FOL, die das nicht ist, gibt es nur gültige Ausdrücke aus und ein Ausdruck, dessen Negation gültig ist, ist ein Widerspruch, keine Tautologie. Vollständigkeit impliziert Entscheidbarkeit nur in der Arithmetik, nicht in der Logik
Dieser Beitrag geht näher auf den Unterschied zwischen diesen beiden Arten von Systemen ein. Philosophy.stackexchange.com/questions/15525/… Ein vollständiges Logiksystem (das jeden der gültigen Ausdrücke dieser Logik ausgibt) impliziert keine Entscheidbarkeit (da es Ihnen sagt, wann ein Ausdruck gültig oder widersprüchlich ist, aber nicht wann ist nur erfüllbar). Wenn ich sage, dass ich denke, dass er zwei verschiedene Arten von Systemen gleichsetzt, beziehe ich mich genau auf diesen Unterschied.
Ich glaube nicht, dass er sich um Erfüllbarkeit kümmert. "Vollständigkeit" bedeutet hier nur, dass alles beweisbar oder widerlegbar ist, also impliziert es per Definition "Entscheidbarkeit" für Arithmetik und Logik gleichermaßen.
Vollständigkeit in einem logischen System bedeutet, dass das System jeden gültigen Ausdruck der Logik einzeln ausgeben kann. Auch hier bedeutet Vollständigkeit in einem logischen System nicht Entscheidbarkeit. Ein "gerade erfüllbarer" Ausdruck wird niemals auf den Beweisen erscheinen und man kann ihn nicht wissen, da es ein gültiger Ausdruck sein könnte, der einfach noch nicht erschienen ist. Auch hier gilt das Argument, das Turing vorbringt, für Axiomatisierungen der Arithmetik, aber nicht für Axiomatisierungen der Logik.
Turings Aufsatz stammt aus dem Jahr 1936. Was heute in einem logischen System im Unterschied zu einem mathematischen System mit Vollständigkeit gemeint ist, ist umstritten, nur das, was er meint, ist von Bedeutung. Und „Vollständigkeit“, wie Turing das Wort verwendet, impliziert Entscheidbarkeit.
Die beiden sind stark miteinander verbunden: Wenn PA die Konjunktion von Axiomen der Arithmetik erster Ordnung und T eine Formel der Arithmetik ist, haben wir, dass PA T genau dann beweist, wenn PA, dann ist T eine gültige FO-Formel.
@MauroALLEGRANZA: Das ist falsch. PA ist nicht endlich axiomatisierbar. Siehe jedoch meine Antwort; Robinsons Arithmetik (und auch TC) ist endlich axiomatisierbar.

Antworten (2)

Was er wahrscheinlich erreichen möchte, ist, dass es eine Möglichkeit gibt, die Vorstellung, dass 𐌵 ein beweisbarer Satz in K ist, in Arithmetik zu codieren, sodass, wenn die Arithmetik vollständig wäre, dieser Satz in Arithmetik bewiesen oder widerlegt werden könnte.

Sie haben absolut recht. Gödel zeigte (über sein β-Lemma), dass man endliche Folgen natürlicher Zahlen als natürliche Zahlen codieren und sie alle innerhalb von PA (oder Äquivalent) manipulieren kann. Ein Beweis in jeder berechenbaren FOL-Theorie T ist einfach eine Folge von Formeln, die die Inferenzregeln erfüllen, die offensichtlich als endliche Folge natürlicher Zahlen kodiert werden können. Ob eine natürliche Zahl einen Beweis über T codiert oder nicht, ist außerdem ein Σ1-Satz (dh von der Form "∃k ( ... )", wobei alle Quantoren in "..." beschränkt sind). Nun ist PA Σ1-vollständig, was bedeutet, dass wenn ein Σ1-Satz wahr ist, PA ihn beweisen kann. Also, wenn T etwas beweist, dann kann PA diese Tatsache beweisen!

Symbolisch gilt für jedes berechenbare formale System T und jeden Satz Q über T, wenn ( T ⊢ Q ) dann ( PA ⊢ ProvT ), wobei Prov[T] ein Prädikat in der Sprache von PA ist.

Nun sollte klar sein, dass das Problem im Fall ( T ⊬ Q ) liegt; wo wir keine Garantie dafür haben ( PA ⊢ ¬ProvT ). (Und tatsächlich zeigte Gödel, dass es im Allgemeinen nicht wahr ist.)

Aber Turings Kommentar kann dahingehend verstärkt werden, dass, wenn es eine berechenbare konsistente Erweiterung E von PA gibt, die jeden wahren Σ1-Satz beweist und jeden falschen Σ1-Satz widerlegt, wir bestimmen können, ob ( T ⊢ Q ) durch einfaches Aufzählen aller Theoreme von E bis wir entweder einen Beweis oder eine Widerlegung von ProvT finden.

Sein ursprünglicher schwächerer Kommentar ist einfach, dass es keine berechenbare konsistente vollständige Axiomatisierung der natürlichen Zahlen N (dh ein Modell von PA) gibt. Aber auch nur nach der Fähigkeit zu fragen, jeden falschen Σ1-Satz widerlegen zu können, ist schlimm genug, wie oben erklärt. All dies stützt sich immer noch auf Gödels β-Lemma, aber die Erklärung ist etwas einfacher. Man braucht nur das ( T ⊢ Q ) gdw ( N ⊨ ProvT ).

Im Zusammenhang mit Ihrer Frage möchte ich auch erwähnen, dass man die Unentscheidbarkeit von FOL direkt über das Gödel-Rosser-Theorem beweisen kann, das auf Robinsons Arithmetik RA angewendet wird. RA ist endlich axiomatisierbar, daher ist die Beweisbarkeit eines Satzes Q über RA gleichbedeutend mit der Beweisbarkeit eines einzelnen Satzes über reinem FOL (dh die Konjunktion der Axiome von RA impliziert Q). Da die Beweisbarkeit von RA nach Gödel-Rosser unentscheidbar ist, ist auch die Beweisbarkeit über reines FOL unentscheidbar.

Wenn Sie an dem vollständig verallgemeinerten Unvollständigkeitssatz von Gödel-Rosser interessiert sind, finden Sie in diesem Beitrag einen einfachen berechenbaren Beweis.

Vielen Dank für Ihre sorgfältige Antwort. Ich werde mir den Blog-Beitrag ansehen, den Sie freundlicherweise geteilt haben. Nur eine Zusatzfrage, der letzte Absatz Ihrer Erklärung war mir nicht ganz klar. Ich bin mir bewusst, dass die Beweisbarkeit eines arithmetischen Satzes, sobald er als FOL-Sätze angegeben ist, der Beweisbarkeit eines gültigen FOL-Satzes entspricht. Dies schließt jedoch nicht die Möglichkeit aus, dass ein Begriff der logischen Gültigkeit nicht innerhalb des spezifischen RA-Modells erfasst wird. Warum die Notwendigkeit, dass es endlich axiomatisierbar sein muss.
@JavierDiego-Fernández: Was Sie in Ihrem zweiten Satz gesagt haben, ist nicht wahr. Die Beweisbarkeit erfolgt immer über ein bestimmtes formales System. Man kann nicht einfach "beweisbar" sagen. Beweisbar über was? Und es scheint, dass Sie auch grundlegende Missverständnisse über logische Gültigkeit und Modelle haben. Wie auch immer, hier ist, was wahr ist: RA ist endlich axiomatisiert, also haben wir ( RA ⊢ Q ) iff ( ⊢ RAX⇒Q ), wobei RAX die Konjunktion der Axiome von RA ist. Mit PA ist dies nicht möglich, da es unendlich viele Axiome hat (und es keine unendliche Konjunktion gibt).

Was er wahrscheinlich erreichen möchte, ist, dass es eine Möglichkeit gibt, die Vorstellung, dass 𐌵 ein beweisbarer Satz in K ist, in Arithmetik zu codieren, sodass, wenn die Arithmetik vollständig wäre, dieser Satz in Arithmetik bewiesen oder widerlegt werden könnte.

Ich glaube nicht, dass er darauf hinaus will. Was er anscheinend vorschlägt, ist, dass Sie ein Computerprogramm schreiben könnten, das jeden möglichen Beweis rekursiv aufzählt ( z Umgang mit Axiomenschemata ). Dies ist eine allgemeine Technik, die es "egal macht", wie Ihre Axiome aussehen. Wenn Sie wissen, dass das System, was auch immer es codiert, vollständig ist (dass es jede Aussage oder ihre Negation beweist) und konsistent (dass es niemals eine Aussage und ihre Negation beweist), dann wird diese Technik immer einen Beweis oder eine Widerlegung jeder Aussage finden Sie möchten danach fragen.

Wie Turing jedoch einräumt, hatte Gödel bereits bewiesen, dass jedes System, das Arithmetik kodieren kann, nicht vollständig und konsistent sein kann, also funktioniert dies nicht wirklich. Turings Argument beweist dann die stärkere Behauptung, dass es keinen Algorithmus gibt, der in diesem Fall funktioniert.

Hallo! Ich habe Ihren Kommentar hier bemerkt und möchte darauf antworten, möchte aber keine unerwünschte Aufmerksamkeit von den Spinnern dort drüben erregen (ich denke, Sie wissen, auf wen ich mich beziehe). Ihre Skepsis ist falsch, und vermutlich liegt es daran, dass Sie mit mathematischer Logik und ZFC eigentlich nicht vertraut sind. Es ist trivial, TMs auf einigermaßen natürliche Weise (dh ohne Gödel-Kodierung) in ACA zu formalisieren und substanziell zu argumentieren, was ein klar prädikatives Fragment der Arithmetik zweiter Ordnung Z2 ist, die viel schwächer als ZFC ist .
In Bezug auf die Festigkeit ist PA = ACA0 < ACA << ATR << Z2 << ZC << ZFC. Mit der Gödel-Codierung kann man tatsächlich über TMs in PA (und in jedem System, das PA interpretiert) 'behaupten'. So erhalten wir PA ⊢ Con(PA)⇒¬⬜Con(PA) wobei "⬜" das Beweisbarkeitsprädikat ist. Sie haben Recht, dass diese Theoreme lediglich Diagonalisierungsargumente sind (Modulo-Codierungs- und Simulationsprobleme), und genau deshalb sind Gödels Unvollständigkeitstheoreme in so schwachen Metasystemen beweisbar. ACA beweist, dass jede berechenbare Teilmenge von N, die eine Theorie kodiert, die PA− interpretiert, entweder inkonsistent oder unvollständig ist.
PA allein kann den Unvollständigkeitssatz für jedes spezifische berechenbare formale System beweisen, das PA berechenbar interpretiert (dh bei einem Computerprogramm, das ein Beweisverifizierer oder ein Theoremgenerator für ein formales System ist, und ein Programm, das eine Übersetzung arithmetischer Sätze in dieses ist System, das bezeugt, dass es PA− interpretiert), können wir über PA einen Beweis konstruieren, dass die zugehörige Theorie widersprüchlich oder unvollständig ist), und zwar rechnerisch (d. h. wir können ein einzelnes Programm aufschreiben, das die Programme für das formale System und gegeben hat Übersetzung gibt den gewünschten Beweis aus).
Vielleicht interessieren Sie sich für weitere Details zu den Unvollständigkeitssätzen in diesem Beitrag und zu ACA hier . Wenn Sie weitere Fragen haben, sind Sie auch in diesem Chatroom willkommen.
Warum behauptet Turing, dass eine vollständige und berechenbare Axiomatisierung der Arithmetik die Entscheidbarkeit der Logik erster Ordnung implizieren würde?
AntwortenHierDatenschutz-Bestimmungen1y, 1v