Wie wird Gödels Unvollständigkeitssatz in der intuitionistischen Logik interpretiert?

Klassischerweise stellt man ein Axiomatiksystem mit einem formalen Deduktionssystem & einer Interpretation in einem Modell auf. Generell gilt: Ein formal abgeleitetes Theorem ist auch wahr, wenn es im Modell interpretiert wird . Die Umkehrung heißt Vollständigkeit, wenn ein Satz im Modell wahr ist, dann ist er auch formal ableitbar. Dies ist die Aussage von Gödels Vollständigkeitssatz .

Verwirrenderweise bezieht sich das Gödel-Unvollständigkeitstheorem auf den Begriff der Entscheidbarkeit (dieser unterscheidet sich vom Begriff der Entscheidbarkeit in der Berechnungstheorie, auch bekannt als Turing-Maschinen und dergleichen) – eine Aussage ist entscheidbar, wenn wir in der Lage sind, festzustellen (zu entscheiden), dass sie entweder einen Beweis hat oder eine Widerlegung. Wenn alle Aussagen in der Sprache entscheidbar sind, nennen wir sie vollständig. Der Satz besagt, dass axiomatische Systeme, die PA enthalten, unvollständig sind – das heißt, es gibt immer Aussagen, die wir weder beweisen noch widerlegen können.

Was passiert nun, wenn das formale Deduktionssystem nicht klassisch, sondern intuitionistisch ist? Die intuitionistische Logik ist vielwertig, aber anstatt die Wahrheit zu modellieren, modelliert man die Konstruierbarkeit/Beweisbarkeit, die anstelle der mengentheoretischen Semantik die Kripke-Semantik verwendet. Jetzt:

  1. Ist es noch Ton ? Das heißt: Ein formal abgeleiteter Satz ist auch konstruierbar?

  2. Ist es unvollständig ? Es gibt einen konstruierbaren Satz, der formal nicht ableitbar ist?

  3. Hat es unentscheidbare Aussagen?

Alles andere als gut gelesen zu diesem Thema, aber die SEP-Seite zum Intuitionismus enthält einige Erwähnungen des Unvollständigkeitssatzes und könnte hilfreich sein.
Wie in den Antworten erwähnt, gelten Goedles Unvollständigkeitstheoreme nur dann für die Intuitionistische Logik , wenn sie als eine Art klassische Logik ohne LEM formalisiert werden , aber dies erfasst nicht den Intuitionismus, wie Brewer vorgeschlagen hat. Im Wesentlichen ist IL nicht nur klassische Logik ohne LEM, da die Semantik anders ist als nur ein paar Änderungen i (i. modifiziere ein paar Regeln) in der Syntax.
Darüber hinaus ist konstruktive Manthematik nicht nur klassische Mathematik ohne Axiom of Choice (was LEM impliziert), sondern in Zitaten wird diese Analogie hergestellt. Es verkörpert vor allem eine andere Sichtweise in Bezug auf die Semantik. In diesem Sinne bettet das Vorhandensein von Sätzen, die unentscheidbar sein können, effektiv Goedes Theoreme als integralen Bestandteil des Intiotionismus von Anfang an ein
ein schöner Beitrag "Gödels Beweis und Intuitionismus" in der gleichen Richtung und Bedeutung wie meine vorherigen Kommentare ( ähnliche Frage zu math.SE )

Antworten (3)

Die gängigen Axiomensysteme für die intuitionistische Logik sind sowohl solide als auch vollständig . Es kann als S4- Modallogik oder als Schwächung der klassischen Logik interpretiert werden (im Wesentlichen lassen Sie einfach das Gesetz der ausgeschlossenen mittleren und doppelten Negationseliminierung fallen und optimieren dann die Quantifiziererregeln).

Da es sowohl solide als auch vollständig ist, ist es nicht unvollständig. Die Tatsache, dass sie "Wahrheit" als so etwas wie "Beweisbarkeit" behandeln, trägt nicht zur Situation bei.

Ist die intuitionistische Logik nun unvollständig? Nein, aber klassische Logik erster Ordnung ist es auch nicht, und Unvollständigkeit tritt tendenziell bei stärkeren logischen Systemen als FOL auf, nicht bei schwächeren.

Die Frage, die Sie meiner Meinung nach im Sinn haben (obwohl ich mich dafür entschuldige, dass ich annehme, Ihre Gedanken lesen zu können), ist, ob intuitionistische/konstruktive Mathematik anfällig für Unvollständigkeit ist. Die Antwort hier ist ja. Gödel lieferte die Beweise auf eine konstruktiv/intuitionistisch akzeptable Weise (dh nur unter Verwendung von Folgerungen, die sie befürworten), und daher würde das Ergebnis für die intuitionistische Zahlentheorie gelten.

Es ist erwähnenswert, dass Sie keine so starke Arithmetik wie PA benötigen, um der Unvollständigkeit zum Opfer zu fallen. Es bedarf lediglich einer Zahlentheorie, die rekursiv axiomatisierbar ist.

Robinson-Arithmetik (Q) ist eine viel schwächere Theorie als PA (ich glaube, es ist PA ohne Induktion), aber es tritt immer noch Unvollständigkeit auf. Es könnte (ich kann mich nicht genau erinnern) das schwächste System sein, das immer noch Opfer der Unvollständigkeitstheoreme ist. Es wurde eigentlich als solch ein schwaches System entworfen – ein System, das alle und nur rekursive zahlentheoretische Funktionen darstellen kann.

Hier ist ein interessanter Artikel, den ich zu diesem Thema gefunden habe – sieht nach einer guten Lektüre aus. Diese Vorlesungsnotizen (wieder von Kevin Klement) machen einen ziemlich guten Job, wenn Sie durch Gödels Theoreme gehen, wenn Sie das wollen. Ansonsten sollte auch der verlinkte SEP-Eintrag @commando hilfreich sein.

danke für die Referenzen, sie sehen nützlich aus. Keine Notwendigkeit, sich zu entschuldigen - Sie haben meine Absichten richtig gelesen! Ich glaube, ich habe die Vollständigkeit verwechselt, die sich auf Syntax und Semantik bezieht, und die Unvollständigkeit, die sich ausschließlich auf die Syntax des „formalen Beweises“ bezieht, nur durch das Inferenz- / Deduktiv- / Beweissystem, wenn ich Sie richtig gelesen habe. Welches ist der zu verwendende Standardname - Inferenz / Deduktiv / Beweis - sie scheinen alle verwendet zu werden?!
@MoziburUllah Ich fürchte, ich verstehe nicht ganz, auf welchen Unterschied Sie hinweisen. Soweit ich weiß, gibt es nur eine Form von (Un)vollständigkeit: (nicht) in der Lage zu sein, jede Wahrheit Ihrer Theorie formal zu beweisen.
Sie sagten "es ist sowohl gesund als auch vollständig, es ist nicht unvollständig " und dann "ob es anfällig für Unvollständigkeit ist . Die Antwort hier ist ja". Ich denke, es sind diese beiden Begriffe von Vollständigkeit, die ich verwechselt habe - einfach, weil sie ähnliche Namen haben.
@Dennis Ich finde es überraschend, dass die intuitionistische Logik vollständig ist, die konstruktive Mathematik jedoch nicht, was bedeuten würde, dass es zusätzliche Axiome gibt, die die Unvollständigkeit verursachen?
@mcb Das ist eigentlich gar nicht so überraschend. (Klassische) Logik erster Ordnung ist die Sprache, in der die meisten Mathematik formalisiert sind. Die Logik erster Ordnung ist vollständig, aber nur sehr wenige mathematische Theorien, die darin enthalten sind, werden es sein. Also ja, Sie haben Recht, es gibt zusätzliche Axiome, die Sie einer Basis intuitionistischer Logik hinzufügen, die die Unvollständigkeit konstruktiver Mathematik verursachen. Insbesondere alle Axiome, die Sie hinzufügen, die es Ihnen ermöglichen, eine Arithmetik zu definieren, die mindestens so stark ist wie die Robinson-Arithmetik, sind die Axiome, die dazu führen, dass der Unvollständigkeitssatz gilt.
@Dennis Die Logik erster Ordnung ist die Sprache, in der die meisten Mathematik formalisiert sind. Ich denke, die meiste Mathematik ist tatsächlich in einer sogenannten "Logik zweiter Ordnung" formalisiert, da Sie ziemlich oft ernsthaft über Funktionssymbole quantifizieren müssen.
@DavidTonhofer Ja, ich glaube, ich habe meinen Fall in diesem Beitrag etwas übertrieben. Oberflächlich betrachtet ist die meiste Mathematik in eine Form erster Ordnung gegossen und die Standardsemantik ist eine mengentheoretische, bei der die „Entitäten zweiter Ordnung“ (Eigenschaften, Funktionen, Beziehungen usw.) als Entitäten erster Ordnung – Mengen – behandelt werden verschiedener Art (z. B. ist eine zweistellige Relation nur eine Menge geordneter Paare, eine Funktion ist nur eine Menge geordneter Paare, wobei das erste Element des Paars nie mit mehr als einem anderen Objekt in Beziehung steht usw.) (Forts .)
Natürlich ist die üblichste Semantik für die Logik zweiter Ordnung jedoch mengentheoretisch, und das trübt das Wasser wirklich. In den Jahren, seit ich diese Antwort gepostet habe, war ich etwas verwirrt darüber, worauf der Streit zwischen Logik erster und zweiter Ordnung hinausläuft. Ist eine Theorie zweiter Ordnung, wenn sie syntaktisch zweiter Ordnung ist, aber scheinbar eine Semantik erster Ordnung hat? Vergessen Sie die vollständige Semantik zweiter Ordnung und betrachten Sie einfach die Henkin-Semantik. Das ist nachweislich auf Logik erster Ordnung reduzierbar und scheint daher eine Unterscheidung ohne Unterschied zu sein. (Fortsetzung)
Der entscheidende Unterschied scheint zu sein, ob die Semantik den Begriff einer willkürlichen Teilmenge/Eigenschaft/Pluralität anspricht – dh ob es sich um die vollständige Semantik für SOL handelt. Das geht eindeutig über die Logik erster Ordnung hinaus. Aber es ist mir immer noch nicht klar, dass es über die Mengentheorie erster Ordnung hinausgeht, insbesondere angesichts der Tatsache, dass Sie in beiden Fällen vollkommen parallele Fragen haben, zB zur Kontinuumshypothese - es geht nur darum, ob sich diese Fragen stellen die Objekt- oder Metasprache. (Fortsetzung)
Ich denke, das einzige, dessen ich mir einigermaßen sicher bin, ist, dass FOL die bessere Logik zum Erfassen von Schlussfolgerungsmustern ist und SOL die bessere Logik zum Umgang mit Fragen der Definierbarkeit und Bedeutung. Im Wesentlichen ist es die Trennung zwischen Syntax und Semantik. Wenn Sie denken, dass die syntaktische (deduktive) Folgerung das A und O der Logik ist, gehen Sie zur ersten Ordnung. Wenn Sie der Meinung sind, dass es bei der Logik darum geht, bestimmte Konzepte zu modellieren, insbesondere kategoriale Theorien zu diesen Konzepten zu entwickeln, dann ist vielleicht die Logik zweiter Ordnung der richtige Weg. (Fortsetzung)
Durchsetzt mit all dem sind schwierige Fragen, wo die Grenze zwischen Logik und Mathematik gezogen werden soll. Natürlich ist FOL Logik, aber was ist mit einer eigenschaftstheoretischen Interpretation der Logik zweiter Ordnung? Das mag gut erscheinen, aber die mengentheoretischen Interpretationen wurden gemeinhin als zu weit in die mathematische Richtung betrachtet (z. B. Quine über die Logik zweiter Ordnung als „Mengentheorie im Schafspelz“). TL;DR Die Philosophie bleibt hart.
(Vorerst letzter Kommentar zu diesen Angelegenheiten.) Ich gebe Ihnen definitiv zu, dass die meiste gewöhnliche Mathematik – dh alles außerhalb der mathematischen Logik und ein Teil des Rests der reinen Mathematik – etwas weniger formell und auf eine solche Weise durchgeführt wird scheint einer Behandlung zweiter Ordnung zugänglicher zu sein (insofern scheinen sie, wie Sie sagen, über Funktionen zu quantifizieren). Ich weiß jedoch nicht, inwieweit sich diese Mathematiker als in einem System erster oder zweiter Ordnung arbeitend begreifen. Das ist keine skeptische Sorge, nur ein echtes bisschen Ignoranz.
Berücksichtigen Sie in Bezug auf Ihren Kommentar, dass die meisten Mathematiker die Induktion nicht als Schema erster Ordnung verwenden, sondern sie als ein einziges Axiom betrachten, das die Induktion für jede Eigenschaft der natürlichen Zahlen angibt . Dies ist wohl metalogischer Natur, was in etwa so ist, als hätte man eine Logik höherer Ordnung mit Henkin-Semantik. Aus diesem Grund werden die meisten von ihnen es "das Axiom der Induktion" und nicht "eine Instanz des Axiomschemas der Induktion" nennen.

Die beiden Begriffe (Vollständigkeit und Unvollständigkeit) sind keine Gegensätze, sondern sehr stark miteinander verbunden (nicht nur durch Gödels Namen im Namen der beiden Theoreme).

Berücksichtigen Sie, dass Gödels Vollständigkeit Th der Logik erster Ordnung lautet:
Wenn ein Satz in allen Modellen der Axiome wahr ist (dh eine logische Konsequenz der Axiome ist), dann ist er auch formal (in FOL) durch die ableitbar Axiome.

Gödels Unvollständigkeit Th bezieht sich auf formale Systeme, die „eine gewisse Menge“ an Arithmetik enthalten (zum Beispiel: Robinson-Arithmetik, die schwächer ist als die von Peano) und besagt, dass wir auf effektive Weise eine in diesen formalen Systemen ausdrückbare Aussage finden können, die „wahr“ ist " im beabsichtigten Modell (dh dem Modell mit Definitionsbereich der Standardzahlen und Operation der Standardaddition und -multiplikation), aber nicht aus den Axiomen ableitbar.

Dies widerspricht nicht der Vollständigkeit Th: Die oben genannte Aussage ist im Standardmodell wahr, aber NICHT in einigen anderen "seltsamen" Modellen (es gibt viele): Dies ist der Grund, warum sie nicht aus den genannten Axiomen abgeleitet werden kann.

Die von Gödel in seinem Beweis konstruierte arithmetische Aussage ist ziemlich "seltsam", aber ausgehend von einem Ergebnis von Paris & Harrington (1977) war es möglich, in der mathematischen Logik Aussagen zu finden, die (im Standardmodell) wahr, aber nicht beweisbar sind in der Peano-Arithmetik und sind "natürlicher". Dies war das erste "natürliche" Beispiel einer wahren Aussage über die ganzen Zahlen, die in der Sprache der Arithmetik angegeben, aber in der Peano-Arithmetik nicht bewiesen werden konnte.

Ich hoffe, Sie haben nichts gegen meine Bearbeitung, um Ihren ersten Satz zu verdeutlichen. Nebenbei habe ich auch einiges an Grammatik und Rechtschreibung korrigiert. =)

(adaptiert von einem Post von mir auf MathSE)

ANMERKUNG 1 Intuitionistische Logik ist NICHT mehrwertig! (und tatsächlich steht Gödels Name wieder im Zusammenhang mit Untersuchungen in dieser Richtung)

Sind die Unvollständigkeitssätze von Gödel sowohl für die klassische als auch für die intuitionistische Logik gültig?

In gewisser Weise JA.

ABER

  1. Gödels Unvollständigkeitssatz(e) gelten zunächst für die klassische Logik

  2. Goedels Unvollständigkeitssatz und sein Beweis sind konstruktiv , aber nicht intuitiv konstruktiv ( Goedels Artikel )

Wieso den?

Gödel selbst erklärte in seinem Referat, dass das obige Vorgehen jedoch „ konstruktiv nicht zu beanstanden “ sei

a) Goedels Hinweis auf den Konstruktivismus (Intuitionismus) ist eher formal als tatsächlich (weiter unten ausführlicher)

b) Variationen von LEM (Gesetz der ausgeschlossenen Mitte) werden in Gödels Beweis verwendet

c) kombiniert mit der Verwendung eines Diagonalisierungsverfahrens

(siehe auch Gödels Beweis und Intuitionismus für eine andere Analyse)

Gilt dies auch für die intuitionistische Logik?

In gewisser Weise JA.

ABER

  1. Goedels negative Übersetzung der klassischen Logik in intuitionistische Logik ist nur formal ( Goedels Artikel )

Wieso den?

a) Die negative Übersetzung der klassischen Logik in die intuitionistische Logik ist kein Intuitionismus , sondern eine formale Analogie , denn die Semantik dessen, was eine Konstruktion, einen Beweis, eine Implikation und natürlich die Definition/Konstruktion neuer Entitäten ausmacht, basiert ausschließlich auf zuvor konstruierten Entitäten anders, klassisch als intuitionistisch (und dasselbe gilt für den ursprünglichen Unvollständigkeitsbeweis, bei dem diese Bedingungen weder formalisiert noch erfüllt sind) (siehe auch Kolmogorovs Interpretation der intuitionistischen Logik als Probleme )

b) Der Intuitionismus hat gewissermaßen die Unvollständigkeitssätze bereits eingebettet, da er Aussagen akzeptiert, die (zu einem bestimmten Zeitpunkt) weder bewiesen noch widerlegt werden können.

c) Brouwer selbst sah Gödels Ergebnisse um mindestens ein Jahrzehnt voraus (Anmerkung: Gödel selbst hatte Brouwers Vorlesungen über die Grundlagen der Mathematik besucht)

Zitieren aus Artemovs Verständnis der konstruktiven Sematik (Spinoza-Vorlesung)

Geben Sie hier die Bildbeschreibung ein

Und auch von hier

Intuitionistische vs. klassische Perspektive

Intuitionisten gründen ihre formalen Systeme normalerweise eher auf Intuition konstruktiver, z. B. informeller Semantik im BHK-Stil , als auf klassische Grundlagen ...

Klassische Mathematiker (wie Gödel, Kolmogorov, Kleene, Novikov und andere) streben nach einem strengen Ansatz

klassische Definition der konstruktiven Semantik.

Im Lichte des Obigen gelten Gödels Unvollständigkeitsergebnisse zwar formal für die intuitionistische Logik (mit klassischer Semantik), nicht aber für den Intuitionismus (der ohnehin kein Unvollständigkeitsergebnis benötigt, da sie bereits in die Praxis und Semantik eingebettet sind)

Wie wird Gödels Unvollständigkeitssatz in der intuitionistischen Logik interpretiert?
AntwortenHierDatenschutz-Bestimmungen1y, 0v