Warum kann ein Algorithmus Unvollständigkeit nicht verstehen?

Was den Unvollständigkeitssatz von Gödel betrifft, müssen wir zuerst mit angemessener Genauigkeit verstehen, was er aussagt; siehe Torkel Franzén, Gödel's theorem An complete guide to its use and abuse (2005):

Erster Unvollständigkeitssatz (Gödel-Rosser) . Jedes konsistente formale System S, innerhalb dessen ein gewisses Maß an elementarer Arithmetik durchgeführt werden kann, ist hinsichtlich elementarer arithmetischer Aussagen unvollständig: Es gibt solche Aussagen, die in S weder bewiesen noch widerlegt werden können.

Schlüsselbegriffe sind: formales System , Konsistenz und „ein gewisses Maß an elementarer Arithmetik“.

Zum ersten:

In populären Formulierungen des Satzes von Gödel wird eine solche Bedingung (was die Axiome betrifft) [über die "Mechanisierbarkeit des Denkens in einem formalen System]" manchmal in Form einer Bestimmung enthalten, dass die Axiome eines formalen Systems sind endlich in der Zahl. Dies impliziert, dass ein Axiom (im Prinzip) als solches erkannt werden kann, indem man eine endliche Tabelle durchsieht. Aber diese Bedingung wird von vielen der formalen Systeme, die in der Logik untersucht werden, wie PA und ZF, tatsächlich nicht erfüllt Diese Systeme haben unendlich viele Axiome, aber es ist immer noch eine mechanische Angelegenheit zu prüfen, ob ein bestimmter Satz ein Axiom ist oder nicht.

Über „ein gewisses Maß an elementarer Arithmetik“ lässt sich diese Vorstellung präzisieren; grob :

Jedes System, dessen Sprache die Sprache der elementaren Arithmetik enthält und dessen Theoreme einige grundlegende Tatsachen über die natürlichen Zahlen enthalten, ist sicherlich eines, das die Bedingung erfüllt.

Was der Satz beweist, ist, dass wir unter den obigen Annahmen „effektiv“ eine Formel G in der Sprache des formalen Systems S aufbauen können (dh eine Formel „aus“ Zahlen und Operationen auf ihnen, dh + und x), wie z daß weder die obige Formel im System beweisbar (dh mit den üblichen Schlußregeln aus den Axiomen des Systems ableitbar) ist, noch ihre Negation not-G.

Diese „seltsame“ Formel ist so fabriziert, dass ihre „Interpretation“ eine wahre Aussage ist, weil die Formel „von sich selbst sagt“, dass sie unbeweisbar ist, und sie ist wirklich unbeweisbar; Wenn das System also so funktioniert, wie wir es wollen, muss die Formel wahr sein.

Na und ? Gödel hat keine "Rechnung gemacht", die unsere Algorithmen nicht durchführen können. Er führte einen mathematischen Beweis mit der üblichen Technik der Mathematik: Einsicht und Argumentation.

Was sein Theorem in Bezug auf das Thema, das wir diskutieren, impliziert, ist, dass die Fähigkeit der mathematischen Logik, die übliche Argumentation, zu der der mathematische (dh menschliche) Verstand in der Lage ist, in einem einzigen formalen System S zu „reproduzieren“, das algorithmisch arbeitet, nicht „gezippt“ werden kann " in ein einziges formales System.

Um die Konstruktion von Gödels Beweis in ein formales System zu formalisieren, müssen wir ein neues (leistungsstärkeres) System S' aufbauen; aber dann können wir die Konstruktion der obigen Formel reproduzieren, was eine neue Formel G' von S' erzeugt, und so weiter.

Dürfen wir auf die Unerschöpflichkeit unseres mathematischen Wissens schließen? Es scheint so [siehe Franzén, Seite 56].

Gödels Unvollständigkeitssatz wird oft grob falsch interpretiert, wenn es um das Thema Intelligenz und künstliche Intelligenz geht.

Sein Theorem besagt, dass es mathematische Aussagen gibt, die weder bewiesen noch widerlegt werden können. Ein Computer, der nach einem Beweis sucht, würde keinen finden. Ein Computer, der nach einem Beweis sucht und nicht aufgibt, würde stecken bleiben. Aber ein brillanter Mathematiker, der nach einem Beweis sucht, würde auch keinen finden. Und wenn dieser Mathematiker nicht aufgab, würde er oder sie auch für immer festsitzen.

Er fand heraus, dass dies Probleme sind, die kein Computer lösen kann. Die gleichen Probleme können jedoch auch von einem Menschen nicht gelöst werden. Manche Leute scheinen zu denken, dass ein unlösbares Problem einer künstlichen Intelligenz Probleme bereiten würde. Aber sicherlich wäre jede künstliche Intelligenz, die diesen Namen verdient, in der Lage, herauszufinden, dass ein Problem schwierig ist, zu schwer, als dass es gelöst werden könnte, und dann, wie es Menschen tun würden, wäre die einzige Möglichkeit, aufzugeben.

Sie haben Recht, das ist nicht der beste Ausdruck für Gödels Ergebnis. Sein Ergebnis ist, dass es keine endlich axiomatisierbare Theorie der Arithmetik gibt. Um einiges auszupacken (aber nicht alles, denn wenn wir alles auspacken, werden wir eine Weile hier sein und ich habe kein Snickers), eine "Theorie der Arithmetik" ist jede Menge von Sätzen, die von einer Sprache erster Ordnung zusammen mit a beinhaltet werden Satz von nicht-logischen Axiomen, die genau die wahren arithmetischen Gleichheiten beinhalten. Eine "endlich axiomatisierbare" Theorie der Arithmetik ist jede Theorie der Arithmetik, für die die Menge der nicht-logischen Axiome eine endliche Größe hat.

Wenn ich es in meinen eigenen, möglichst natursprachlichen Ausdruck fassen müsste, würde ich sagen: „Wenn einem Computer ein Programm gegeben würde, das dazu bestimmt ist, alle und nur die wahren arithmetischen Gleichheiten zu erzeugen, würde es immer eine wahre Gleichheit sein, die es systematisch verfehlen wird."