Diskussion:Beweise der gödelschen Unvollständigkeitssätze

Verwirrend

Erst werden die "Parameter" von Beweis als Beweis(G(Beweis),G(Satz)) eingeführt, später wird aber wohl teils Beweis(G(Satz),G(Beweis)) verwendet. Das müsste noch sortiert werden.--Hagman (Diskussion) 23:29, 2. Mär. 2012 (CET)

Danke für den Hinweis, wird erledigt.--Schreiber ✉ 10:12, 3. Mär. 2012 (CET)

Wo siehtst Du die umgekehrte Variante? Ich habe kein Vorkommen von Beweis(G(Satz),G(Beweis)) finden könne. Grüße--Schreiber ✉ 10:14, 3. Mär. 2012 (CET)

Sorry, habs gefunden.--Schreiber ✉ 10:21, 3. Mär. 2012 (CET)

trennzeichen

zitat: "Die Gödelnummern der Symbole werden durch 0 getrennt, da keine Gödelnummer eines Symbols eine 0 enthält. Damit kann jede Formel eindeutig aus ihrer Gödelnummer rekonstruiert werden." das ist doch voellig unnoetig, da alle symbole durch eine dreistellige zahl dargestellt werden. das habe ich auch hier in der WP zum ersten mal gesehen. gibt es dafuer einen guten grund den ich uebersehen habe? mMn verschlechtert das sogar die lesbarkeit, ein leerzeichen wuerde genuegen. --Mario d 17:50, 1. Mai 2012 (CEST)

Ja, scheint mir auch sinnlos, hab es aber beim Übersetzen aus en mal so gelassen, weil ich die Methode im Gegensatz zu Verfahren mit Potenzen leicht verständlich fand, aber das Buch von Hofstadter nicht da hatte. Die Nummern werd ich auch gleich mal vereinfachen, die wirken ja in dieser Form hier auch völlig unmotiviert. Gruß--Schreiber ✉ 18:45, 1. Mai 2012 (CEST)

die dreistelligen zahlen sind sinnvoll, wenn man GEB gelesen hat, aber fuer die paar formeln reicht auch die fortlaufende nummerierung. die trenn-null hast du ja gleich mitaufgeraeumt, also problem geloest. --Mario d 19:58, 1. Mai 2012 (CEST)

Danke für das elimieren der 20, hatte ich ganz übersehen.--Schreiber ✉ 20:07, 1. Mai 2012 (CEST)

Kritikliste

Also, hier also meine angekündigter Post. Es gibt zwei Teile. Im ersten Teil stehen die substantiellen Sachen, im zweiten Teil dann die kleineren Dinge, die man immer so einem Artikel findet oder auch einfach nur Vorschläge.

@schreiber: Ich las deinen Beitrag erst, als ich schon mit der Liste angefangen hatte. Ich hab erstmal alles, was mir aufgefallen ist, aufgelistet (ohne erstmal genau zu überlegen, wie man das verbessern kann.) Kleinere Dinge kann ich selbstverständlich umsetzen. Manches aber erfordert aber größere Änderungen und auch Planungen. Für mich ist es auch leichter, erst mal zu schauen, was mE nicht OK ist und sich dann im nächsten Schritt um eine Umsetzung bemühen.

Ich hatte in der Diskussion zu Gödels U-Sätzen geschrieben, dass da einiges durcheinander geht: Man muss bei der Behandlung von Gödels Sätzen sorgsam zwischen

• Metasprache und Objektsprache
• Relationen von Zahlen und deren Repräsentierung in der Objektsprache durch eine Formel
• natürlichen Zahlen und deren Repräsentation in der Objektsprache

unterscheiden.

Letzteres bedeutet, dass wir von einer Formel zu einer natürlichen Zahl über die Göderlisierung gelangen, und dann von dort zu einem Term der Sprache Q.

Außerdem ist es sinnvoll, die Annahmen, die man auf der Metaebene macht, zu verdeutlichen. Wenn ich von der Wahrheit oder der Falschheit gewisser objektsprachlicher Sätze spreche, habe ich eine Semantik im Kopf. Dadurch impliziere ich schon die Konsistenz des Kalküls. Wenn nun die Konsistenz als Voraussetzung explizit erwähne, annehme, so tue ich dann wieder so, als ob ich einen finiten Standpunkt einnehme. Das stiftet Verwirrung.

(Noch ne Anmerkung: Gerade für viele Laien hat der U-Satz einen Reiz durch die scheinbare Selbstbezüglichkeit. Diese dürfte es ja eigentlich der Mathematik nicht geben! Das ist auch bemerkenswert und hat auch die Ironie, dass mit dem U-Satz - und seiner Idee des scheinbaren Selbstbezugs - ein Programm zum Scheitern gebracht wurde, das nicht zuletzt entstand, um die Schwierigkeiten zu beseitigen, die sich aus der Möglichkeit zum Selbstbezug ergaben. Um so mehr sollte ein Beweis deutlich machen, dass dieser Selbstbezug nur auf der informellen, der heuristischen Ebene stattfindet, die Mathematik bemerkt aber - sozusagen - nix davon.)

Letzte Anmerkung: Fast unnötig zu sagen, dass ich bei meiner Aufzählung möglichst penibel bin; lieber einmal zu viel etwas gesagt als zu wenig. Und: Nicht alles hab ich genau begründet, die Begründungen kann ich auf Anfrage aber gerne nachliefern.

Nicht alle gefundenen Fehler beziehen sich auf Verwechslungen dieser Kategorien.

Nun konkret:

1.1 Sei T ein formales System, welches natürliche Zahlen mit Addition und Multiplikation beschreiben kann. Dann gilt eine der folgenden Möglichkeiten:

Was danach kommt, ist falsch. Es können auch beide Möglichkeiten zutreffen.

1.2 Null hat keinen Vorgänger: Sx ≠ 0

So jetzt fangen die Probleme langsam an. Ich halte es für ungünstig, in der Objektsprache dasselbe Zeichen für Gleichheit zu verwenden wie in der Metasprache. Gerade ein Anfänger hat es schwer, die Ebenen auseinander zu halten. Besser ist daher $\neg (Sx\doteq 0)$ wie in der Logik üblich.

1.3 Rekursive Definition von Addition und Multiplikation:

Nein, es handelt sich nicht um eine rekursive Definition, sondern um eine axiomatische Einführung der Addition, um Additionsaxiome.

1.4 sodass für jedes Paar von Zahlen n und m, Beweis(n, m) genau dann wahr ist...

Das ist syntaktischer Unfug. "Beweis(n,m)" ist kein vernünftiger Ausdruck, denn ich kann Zahlen nicht in Formeln einsetzen. Das Problem ist, dass hier nie die Abbildung vorkommt (geschweige denn definiert wird), die einer natürlichen Zahl ihre Repräsentation im Kalkül zuordet. (Verwechslung zwischen Gödelzahl Numeral (s. Ende von 1.4), die noch häufig vorkommt.)

Man könnte zB. rekursiv definieren (bessere Typografie allerdings erforderlich^^):

$c_{0}:='0'$

$c_{n+1}:='S'c_{n}$

Ich nenne mal diese "$c_{i}$" im Rest meines Beitrags hier Numeral.

Um es klar zu sagen: Man kann so eine Vermischung durchziehen ("by abuse of notation"). Aber dann muss man die irgendwo deutlich machen, auch ist das nicht zum Verständnis für Anfänger geeignet. In dem Kontext dieses Artikels, wo schon viele Verwechslungen vorkommen, ist das aber wohl nicht anzuraten.

1.5 Da jede natürliche Zahl durch wiederholte Anwendung der Nachfolgeroperation S auf 0 erhalten werden kann' und 'die Gödelnummer für 4, SSSS0

Nein, die Zeichen können so erhalten werden, aber das "SSSS0" ist keine Zahl, sondern ein Zeichen. Diese Verwechslung zieht sich jetzt durch.

1.6 Da das formale System rekursiv aufzählbar ist

Nein, man braucht hier Entscheidbarkeit für die dann folgende Schlussfolgerung.

1.7 Zudem lässt sich eine Formel Beweis(x,y) definieren, die für zwei Zahlen x and y genau dann wahr

Verwechlung von Ebenen. Einmal sind 'x' und 'y' Variablen der Objektsprache (genauer: Variablen für Variablen), dann Variablen der Metasprache. Auch der Fehler wiederholt sich.

1.8 Beweis(x,y) ist eine arithmetische Relation

Verwechslung von Sprachebenen: Beweis(x,y) ist eine Formel (die vielleicht eine Relation ausdrückt oder bezeichnet), aber keine Relation.

1.9 Die Konstruktion der Formel Beweis hängt entscheidend davon ab, dass die Theorie rekursiv aufzählbar ist

Man braucht mehr als nur rekursive Aufzählbarkeit.

1.10 Dann ist Beweis(n, G(p)) wahr und...

Wahrheit von Formeln wurde noch nicht eingeführt und ist auch nicht das, was hier benötigt wird. Beweisbar reicht.

1.11 p ↔ F(G(p))

Das übliche Verwechslung zwischen Gödelzahl und Numeral.

1.12 Damit ermöglicht das System einerseits die Konstruktion einer Zahl mit einer bestimmten Eigenschaften, aber beweist andererseits für jede Zahl n, dass diese die Eigenschaft nicht hat.

Nein, es konstruiert nicht eine bestimmte Zahl, es beweist ihre Existenz, es beweist einen Existenzsatz.

1.13 Damit ermöglicht das System einerseits die Konstruktion einer Zahl mit einer bestimmten Eigenschaften, aber beweist andererseits für jede Zahl n, dass diese die Eigenschaft nicht hat.

Die alte Verwechslung(zwischen Gödelzahl und Numeral: Das System beweist nicht etwas für jede Zahl n, sondern für jede Zahl n gilt:

$\vdash \neg Beweis(c_{n},c_{G(P)})$

1.14 und das neue System ist wieder entweder ω-inkonsistent oder unvollständig

Das ist falsch. Falls man p dazu nimmt, ist das neue System ω-konsistent und unvollständig, nimmt man $\neg$p hinzu, ist das neue System ω-inkonsistent und konsistent (und unvollständig, dass können wir aber erst nach dem nächsten Absatz mit Rosser beweisen).

1.15 Dann gibt es eine Zahl m < n, die Gödelnummer eines Beweises der Negation von R ist.

Da ist ne Lücke im Beweis. Der Sprung von "Im Kalkül kann ich eine Existenzformel beweisen" zu "Es gibt eine natürliche Zahl mit der entsprechenden Eigenschaft" funktioniert so ohne weiteres nicht, deshalb war es ja gerade erforderlich, das Konzept der ω-Konsistenz einzuführen. Benutzt wird in diesem Schritt ua. die primitive Rekursivität der Beweisbarkeitsrelation. Im weiteren Verlauf die übliche Verwechslung.

Sonstiges:

2.1 Sei T ein formales System, in dem die Robinson-Arithmetik interpretierbar ist

Ich weiß nicht, ob interpretierbar hier so ohne weiteres verstanden wird. Vielleicht ist es besser, von einer konkreten Theorie auszugehen und dann später zu sagen, dass es auch für weitere Theorien gibt.

2.2 welche intuitiv zu einer gegebenen Zahl eins addiert

Sprache, besser: "... welche, intuitiv gesprochen, zu einer..."

2.3 Gödel bewies den Satz ursprünglich für das viel stärkere System der Principia Mathematica.

Das ist, wenn ich mich richtig erinnere, nicht ganz richtig. Der Titel lässt das zwar vermuten, er benutzte aber sein eigenes System. Aber es war klar, dass es um den Anspruch der PM ging und dass sich der Beweis grundsätzlich auch für die PM adaptieren ließ. (Der Kalkül der PM hätte dafür allerdings verbessert werden müssen, er war, was Präzision anbelangt, ein Rückschritt gegenüber Frege, wie ein Logiker (ich glaub Gödel selbst) mal gesagt hat.)

2.4 jeder Formel der Theorie wird eine Zahl

besser: "Jedem Ausdruck der Theorie...", da ja auch Terme gödelisiert werden.

2.5 werden die Nummern der Formeln hintereinander geschrieben und jeweils durch eine Null getrennt

Hier vielleicht der Hinweis, dass diese Form der Gödelisierung aus "Gödel, Esche, Bach" (oder nicht? Bin mir nicht so ganz sicher) ist und zwar leichter zu definieren ist, aber schwerer zu handhaben ist.

2.6 Schlussregeln können als binäre Relationen zwischen Gödelnummern von Folgen von Formeln repräsentiert werden.

Vielleicht ist es nicht schlecht, diese "Repräsentation" zu erklären, da dies eine zentrale Idee von Gödel ist.

2.7 Hierzu lässt sich das Diagonallemma anwenden

Das Diagonallemma ist auch eine zentrale Idee und könnte einen prominenteren Platz bekommen. Vielleicht reicht es, statt "Diagonalisierung" als Überschrift "Das Diagonallemma" zu verwenden.

2.8 Zweiter Unvollständigkeitssatz

Vielleicht nochmal deutlicher darauf hinweisen, dass der 2.te eine Formalisierung des 1. ist.

2.9 Bernays-Löb-Axiomen

Wenn ich mich recht entsinne, kenn ich die unter "Hilbert-Bernayschen-Ableitbarkeitsbedingungen". Vielleicht hier einen Link auf das Buch setzen.

2.10 Alternative Beweise

Hier sollte man mE erwähnen, dass häufig auch der erste U-Satz auf die Unlösbarkeit des Halteproblems zurückgeführt wird, zB im verlinkten wikibook.--Frogfol (Diskussion) 18:13, 29. Jul. 2012 (CEST)

Danke! Als ich den Artikel geschrieben habe, habe ich die Ebenenverwechselungen bewusst in Kauf genommen, 1. weil die Logik-Literatur oft auch nicht ganz so penibel ist und 2. ich dachte, das würde so leichter verständlich. Aber mir ist das sehr recht, wenn das präziser dargetsllt wird. Numerale würde ich dann durch ${\dot {n}}$ repräsentieren, okay? Ähnlich bei 1.2, ich bevorzuge auch diese Notation, aber ich habe nicht den Eindruck, dass das in der Literatur üblich ist (kenne es nur von Hinman), und könnte mir vorstellen, dass wieder jemand kommt und vermeintliche Nichtstandard-Notation bemängelt. Aber von mir aus gerne mit Punkt über allen nichtlogischen Zeichen der Sprache. Zu den sonstigen Punkten:

• 1.1, 1.3 (hab ich so wo gelesen, aber von mir aus) 1.12, 1.14, 2.4, 2.5 hab ich mal erledigt.
• 1.5: Naja, S kann man schon auch als metasprachliche Operation verstehen. Ich würde S in der Objektsprache sowieso dann durchgehend als ${\dot {S}}$ schreiben.
• 1.6, 1.9: Naja, jedes rekursiv aufzählbare System hat eine entscheidbare Axiomatisierung. (Ansonsten: Eine akzeptierende Berechnung kann man ja schon als Beweis verstehen. Ob man Beweisbarkeit über ein Kalkül oder ein Berechnungsmodell formalisiert, ist für die Darstellung hier doch recht unerheblich, so lange der Leser über die Details der Formel "Beweis" mehr oder weniger im Unklaren gelassen wird.)
• 1.15: Die Lücke finde ich sehr gering (verglichen mit den Lücken in den vorangehenden Teilen), aber kann man von mir aus gerne etwas füllen.
• 2.1: Gerade das mit der Interpretierbarkeit macht es so schön allgemein, die Interpretierbarkeit wird ja direkt darunter eklärt.
• 2.6, 2.7, 2.8 2.10: gerne

Gruß--Schreiber ✉ 20:03, 29. Jul. 2012 (CEST)

Gern. Richtig, auch in der Literatur werden die Ebenen nicht manchmal nicht genau auseinander gehalten. Aber in der Anfängerliteratur wird es dann zumindest erwähnt. Und im Artikel hier kann man viele Doppeldeutigkeiten ausschalten und dadurch an - davon bin ich überzeugt - an Verständlichkeit gewinnen. (Vielleicht werden nicht alle zustimmen (was die Verständlichkeit anbelangt), aber wenn ich zB einfach mal in der Analysis implizit voraussetze, dass alle Frunktionen ${\text{C}}^{\infty }$ sind, dann werden die Beweise leichter (zu führen und zu verstehen), aber leider auch "falscher".)

"$\doteq$" kenne ich aus mehreren (Einführungs-)büchern. Sicherlich wird es nicht von allen verwendet. Gerade, wo es hier um verschiedene Sprachebenen und Abbildungen zwischen ihnen geht, halte ich eine Unterscheidung für sehr sinnvoll. (Hier ist dot dann sozusagen eine in der Metametasprache definierte homomorphe Abbildung der Metasprache auf die Objektsprache^^)

zu 1.6, 1.9: "Naja, jedes rekursiv aufzählbare System hat eine entscheidbare Axiomatisierung." Mmh, nicht jede Axiomatisierung eines rekursiv aufzählbaren Systems ist entscheidbar. Aber es reicht doch auch zu sagen bzw zu skizzieren, dass die Relation Bew(x,y) (x ist die Gödelzahl eines Beweises der Formel mit der Gödelzahl y) repräsentierbar ist, also, wenn wir in der dot-Schreibweise bleiben:

falls Bew(x,y) dann $\vdash {\dot {Bew}}({\dot {x}},{\dot {y}})$ und falls non Bew(x,y) dann $\vdash \neg {\dot {Bew}}({\dot {x}},{\dot {y}})$

1.15 Die Lücke ist vielleicht nicht sooo groß, ich hatte den Eindruck, dass hier - wie gesagt - von dem Beweis der Existenz im Kalkül auf die Existenz einer Zahl geschlossen wird. Der naheliegende Schluss:

$\vdash \exists {\dot {x}}{\dot {A}}{\dot {x}}{\text{ also existiert ein n mit A(n)}}$

geht im allgemeinen nur dann, wenn A primitiv rekursiv ist und wir die ω-Konsistenz voraussetzen. Mein Einwand ist nicht so sehr, dass die Lücke zu groß ist, sondern dass man hier leicht zu einem Fehlschluss kommt.--Frogfol (Diskussion) 21:51, 29. Jul. 2012 (CEST)

Okay, dann werde ich das mit dem Punkt schon mal einarbeiten. Für 1.6/1.9: also sagen, dass, da das System rekursiv aufzählbar ist, Bew(x,y) repräsentierbar ist? Die Lücke zu 1.15 werde ich auch mal versuchen zu schließen (für den von dir genannten Schluss braucht man doch nur ω-Konsistenz, die primitiv-Rekursivität ist nicht nötig.) . Gruß--Schreiber ✉ 17:37, 30. Jul. 2012 (CEST)

Erledigt, vielleicht kannst du dir kurz die Änderungen bei Rosser anschauen. Gruß--Schreiber ✉ 18:33, 30. Jul. 2012 (CEST)

Bemerkung: Es gab einen Schreibkonflikt, hab gerade einfach den schon geschriebenen Text reingepastet.

für den von dir genannten Schluss braucht man doch nur ω-Konsistenz, die primitiv-Rekursivität ist nicht nötig.

Nein, man braucht auch die primitiv-Rekursivität, denn ich brauche:

${\text{Für alle n gilt: }}\vdash {\dot {A}}{\dot {n}}{\text{ oder }}\vdash \neg {\dot {A}}{\dot {n}}$

Und das bekomme ich aus der PR. Ich könnte dir ein Gegenbeispiel angeben, das ist aber nicht ganz so leicht. ω-Konsistenz ist nicht Konsistenz in der ω-Logik! (Die Lücke war gewissermaßen in deinen Augen deshalb nicht so groß, weil du sie nicht gesehen hast, no offense.)

Für 1.6/1.9: also sagen, dass, da das System rekursiv aufzählbar ist, Bew(x,y) repräsentierbar ist?

Nein, das ist eben nicht richtig und auch ungenau. Besser imho: Die Axiome sind entscheidbar, also ist die Beweisbarkeitsrelation entscheidbar, also lässt sich die Beweisbarkeit "sehr gut" repräsentieren. Repräsentieren (Übersetzen aus der Metasprache in die Objektsprache) lassen sich erstmal viele Eigenschaften. "Gut" repräsentieren lässt sich eine rekursive Eigenschaft A (zB Beweisbar), dann gilt nämlich:

${\text{Falls A(n), dann }}\vdash {\dot {A}}({\dot {n}})$

"Sehr gut" lassen sich PR-Eigenschaften repräsentieren (zB Beweis(n,m), allerdings 2-stellig), da dann gilt:

${\text{ A(n) gdw }}\vdash {\dot {A}}({\dot {n}})$

Insbesondere gilt: $\vdash {\dot {A}}({\dot {n}}){\text{ oder }}\vdash \neg {\dot {A}}({\dot {n}})$

So in etwa könnte das im Artikel ablaufen. Die Struktur des Artikels finde ich sehr gut, ua. weil man ohne Probleme modular am Text arbeiten kann. Ich werde mal versuchen, Dinge einzupflegen.--Frogfol (Diskussion) 19:02, 30. Jul. 2012 (CEST)

Habe noch etwas zum Halteproblem geschrieben.

Nein, man braucht auch die primitiv-Rekursivität, denn ich brauche:: Äh ja. Was ich meinte war, dass normale Rekursivität reicht, aber was ich dann geschrieben habe war falsch^^ (Aber mit der Lücke im Artikel hat das mit der ω-Konsistenz doch nicht viel zu tun, in der jetzigen Version sehe ich jedenfalls keine Lücke mehr)

Nein, das ist eben nicht richtig und auch ungenau. Besser imho: Die Axiome sind entscheidbar, also ist die Beweisbarkeitsrelation entscheidbar. Okay. Ich hielt es für übermäßig schwer verständlich, erst etwas von rekursiv aufzählbar zu sagen und nachher auch noch zu fordern, dass die Axiome entscheidbar sein sollen. Man braucht Beweis(x,y) ja nur für Beweisbar(x), für das rekursive Aufzählbarkeit reicht, da es egal ist, welche Axiomatisierung wir nehmen. Aber nachdem oben schon die Axiome der Robinson-Arithmetik explizit dasteht, macht es natürlich schon Sinn, auf deren Entscheidbarkeit zu verweisen. Gruß--Schreiber ✉ 19:18, 30. Jul. 2012 (CEST)

(Wir scheinen mit "rekursiv" unterschiedliche Sachen zu meinen. Ich meinte entscheidbar, du anscheinend rekursiv aufzählbar)--Schreiber ✉ 19:20, 30. Jul. 2012 (CEST)

Äh, ja, das ist richtig. Und außerdem: Immmer wenn das Wort "wahr" verwendet wird (auch wenn es nur informell gebraucht wird), leuchten die Alarmglocken bei mir: Widerspruchsfreiheit über die Existenz eines Modells impliziert!

Wie sehr man Rekursivität und Entscheidbarkeit einbaut, muss mE noch geklärt werden. Mein Vorschlag, wie oben beschrieben, könnte man einbauen. Und nein, du brauchst schon die PR von Beweis. Das wird im Artikel durch den Gebrauch von "wahr" etwas verschleiert. Du brauchst es für ${\text{Aus non Beweis(n,m) folgt }}\vdash \neg {\dot {Beweis}}({\dot {n}},{\dot {m}})$

Und Rosser hab ich mir angeschaut und denke noch darüber nach, ich hab da noch ein zwei Verbesserungsvorschläge.--Frogfol (Diskussion) 18:28, 31. Jul. 2012 (CEST)

Hab mal oben etwas gestrafft und versucht, das ganze etwas knackiger auszudrücken.

Da jede natürliche Zahl durch wiederholte Anwendung der Nachfolgeroperation S auf 0 erhalten werden kann, hat jede natürliche Zahl eine Gödelnummer.

ändere ich mal ab. Das ist - jetzt erst recht - nicht richtig.--Frogfol (Diskussion) 19:03, 31. Jul. 2012 (CEST)

Solange man "wahr" für $\Sigma _{1}$-Formeln verwendet, ist das m.E. noch recht unproblematisch, weil "wahr" dann ohne Modell konstruktiv definierbar ist. Aber egal, ich stimme zu, dass man "wahr" im Artikel möglichst vermeiden sollte. PR braucht man wirklich nicht, es genügt, dass die Menge entscheidbar ist. Denn wenn R entscheidbar ist, dann gibt es eine $\Delta _{0}$-Formel $\varphi (x,y,z)$ "Bei Eingabe x hat die Turingmaschine für R im Schritt y den Zustand z" mit:

• R(n) gdw. $\vdash \exists y\varphi ({\dot {n}},y,{\dot {1}})$ (ein akzeptierender Zustand wird erreicht)
• non R(n) gdw. $\vdash \exists y\varphi ({\dot {n}},y,{\dot {0}})$ (ein ablehnender Zustand wird erreicht)
• $\vdash \exists !z\ \varphi (x,y,z)$
• $\vdash (\varphi (x,y,z)\wedge (z\doteq {\dot {0}}\vee z\doteq {\dot {1}}))\rightarrow \forall y'>y\ \varphi (x,y',z)$ (nach Termination ändert sich der Zustand nicht mehr)

Wenn jetzt non R(n) gilt, dann gibt es ${\dot {m}}$ mit $\vdash \varphi ({\dot {n}},{\dot {m}},{\dot {0}})$ und mit der dritten und vierten Aussage kann man herleiten, dass $\vdash \neg \exists y\varphi ({\dot {n}},y,{\dot {1}})$ gilt.

Danke für die Erklärungen zum Punkt und den Numeralen.--Schreiber ✉ 15:02, 1. Aug. 2012 (CEST)

Jetzt bin ich etwas verwirrt, ich kann nicht ausschließen, dass ich eine falsche Definition von PR im Kopf hatte. Sry, wenn wir dadurch aneinander vorbeigeredet haben und ich dir mehr Arbeit bereitet habe.

Ich versuche nochmal, meinen Punkt zu verdeutlichen. Es wird im Artikel folgendes behauptet:

Da das formale System rekursiv aufzählbar ist, kann man effektiv entscheiden, ob eine gegebene Zahl Gödelnummer eines Axioms ist.

Und das ist falsch. Gegenbeispiel: Nimm als Axiome von T' alle aus T beweisbaren Sätze. Dann ist T' aufzählbar aber nicht entscheidbar. Speziell gilt nicht:

$Aus\ non\ Beweis_{T'}(n,m)folgt\ \vdash \neg {\dot {Beweis_{T'}}}({\dot {n}},{\dot {m}})$

Und das braucht man für den Rosser-Beweis später. Also benötigt man, damit der Beweis funktioniert, ein entscheidbares Axiomensystem. Es ist schon klar, wie man dann den Beweis zu ändern hat (durch so eine Formel wie oben bei dir, die die Aufzählung formalisiert.) Aber so ist im Beweis eine Lücke, die dadurch überdeckt wird, dass etwas falsches drin steht.

Okay. Ich hielt es für übermäßig schwer verständlich, erst etwas von rekursiv aufzählbar zu sagen und nachher auch noch zu fordern, dass die Axiome entscheidbar sein sollen.

hattest du oben geschrieben. Der Artikel soll ja nur (kann auch nur) eine Beweisskizze sein. Warum nicht einfach schreiben, dass er für rek-aufzählbare Systeme gilt, er aber hier nur für entscheidbare Axiomensysteme gezeigt wird? Eventuell kann man dann noch später in einem weiteren Abschnitt noch zeigen, wie er dann für aufzählbare Systeme adaptiert werden kann.--Frogfol (Diskussion) 22:23, 1. Aug. 2012 (CEST)

Kein Problem. Die verwirrende Sache ist wohl die, dass Beweise der Unvollständigkeitssätze meist nur die Repräsetierbarkeit für PR-Funktionen zeigen, weil man nur die braucht. Tatsächlich ist diese starke Form der Repräsentierbarkeit aber äquivalent zur Entscheidbarkeit.

• Und das ist falsch. Gegenbeispiel: Stimmt, so formuliert ist das falsch. Mit dem Vorschlag, eine entscheidbare Axiomenmenge vorauszusetzen, bin ich einverstanden.--Schreiber ✉ 11:58, 2. Aug. 2012 (CEST)

Habs eingefügt. Hab ne Zusammenfassung am Ende eines Abschnittes eingefügt. Ich find das nicht schlecht, so macht man sozusagen die Schnittstellen klar. Sprachlich muss das jetzt noch an einigen Stellen geglättet werden.--Frogfol (Diskussion) 22:34, 2. Aug. 2012 (CEST)

Ist der Beweis der Unabhängikeit des Gödelsatzes formalisierbar ?

Wenn man die Konsistenz des formalen Systems nicht voraussetzt, kann man den Beweis der Unabhängigkeit doch auch so formulieren:

Annahme : p ist beweisbar, dann wäre Beweisbar(G(p)) beweisbar. Aber p ist äquivalent zur Negation von Beweisbar˙(G(p)), damit ist eine Aussage und ihre Negation beweisbar. Das ist ein Widerspruch, also muss die ursprüngliche Annahme (p ist beweisbar) falsch sein. Womit die Negation : "p ist nicht beweisbar" bewiesen ist. (Widerspruchsbeweis)

Wenn man jetzt diesen obigen Beweis innerhalb des formalen Systems formalisieren kann (und ich sehe eben nicht, warum das nicht geht), dann ergibt sich damit ein Beweis für p. Also wäre damit gezeigt, dass das formale System widersprüchlich ist. Das würde aber doch dann einfach bedeuten, dass jedes formale System, dass die Arithmetik enthält, widersprüchlich ist. Kann mir jemand erklären, wo in dieser Argumentation der Fehler steckt ? Olivenbaer (Diskussion) 11:38, 5. Feb. 2018 (CET)

Konstruktion oder Überprüfung?

Zitat aus der aktuellen Version: "Die Konstruktion der Formel {\dot {Beweis}} hängt entscheidend davon ab, dass das Axiomensystem entscheidbar ist; ohne diese Annahme wäre die Formel nicht konstruierbar."

Ich habe mir überlegt, wie die Formel aussieht. Wenn ich das richtig verstanden habe, ist die entsprechende Formel für Beweis(x,y) einfach "x impliziert y", also $\neg x\vee y$. (Um genau zu sein: die Formel ist $\neg X\vee Y$, wo X die von x kodierte Formel ist und Y die von y kodierte Formel.) Die Konstruktion davon ist sehr leicht. Die Überprüfung davon ist es unter Umstanden aber nicht, und es ist genau an dieser Stelle, dass wir die Entscheidbarkeit brauchen. Oder?

Wir könnten die Formel für Beweis(x,y) sogar noch einfacher als x 0 y schreiben, weil wir vereinbart haben, dass so eine Formel genau bedeutet, dass Y aus (Aussagen aus) X und/oder Axiomen folgt.

Gerade ist mir aufgefallen, dass es in der Sprache kein Implikationssymbol gibt. Natürlich brauchen wir auch keins, aber es ist vielleicht gut, das im Text zu erklären. Ich werde etwas dazu schreiben. KarlFrei (Diskussion) 11:02, 26. Feb. 2019 (CET)

Habe ich jetzt gemacht. Wieso fehlt aber das Kleiner Dann-Zeichen?? In der englischen Wikipedia ist es da... KarlFrei (Diskussion) 11:08, 26. Feb. 2019 (CET)