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

aus Wikipedia, der freien Enzyklopädie
Letzter Kommentar: vor 5 Jahren von KarlFrei in Abschnitt Konstruktion oder Überprüfung?
Zur Navigation springen Zur Suche springen

Verwirrend

[Quelltext bearbeiten]

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)Beantworten

Danke für den Hinweis, wird erledigt.--Schreiber 10:12, 3. Mär. 2012 (CET)Beantworten
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)Beantworten
Sorry, habs gefunden.--Schreiber 10:21, 3. Mär. 2012 (CET)Beantworten

trennzeichen

[Quelltext bearbeiten]

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)Beantworten

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)Beantworten
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)Beantworten
Danke für das elimieren der 20, hatte ich ganz übersehen.--Schreiber 20:07, 1. Mai 2012 (CEST)Beantworten

Kritikliste

[Quelltext bearbeiten]

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 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^^):

Ich nenne mal diese "" 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 pF(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:

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 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)Beantworten

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 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 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)Beantworten
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 sind, dann werden die Beweise leichter (zu führen und zu verstehen), aber leider auch "falscher".)
"" 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 und falls non Bew(x,y) dann
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:
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)Beantworten
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)Beantworten
Erledigt, vielleicht kannst du dir kurz die Änderungen bei Rosser anschauen. Gruß--Schreiber 18:33, 30. Jul. 2012 (CEST)Beantworten
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:
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:
"Sehr gut" lassen sich PR-Eigenschaften repräsentieren (zB Beweis(n,m), allerdings 2-stellig), da dann gilt:
Insbesondere gilt:
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)Beantworten
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)Beantworten
(Wir scheinen mit "rekursiv" unterschiedliche Sachen zu meinen. Ich meinte entscheidbar, du anscheinend rekursiv aufzählbar)--Schreiber 19:20, 30. Jul. 2012 (CEST)Beantworten
Ä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
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)Beantworten
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)Beantworten
Solange man "wahr" für -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 -Formel "Bei Eingabe x hat die Turingmaschine für R im Schritt y den Zustand z" mit:
  • R(n) gdw. (ein akzeptierender Zustand wird erreicht)
  • non R(n) gdw. (ein ablehnender Zustand wird erreicht)
  • (nach Termination ändert sich der Zustand nicht mehr)
Wenn jetzt non R(n) gilt, dann gibt es mit und mit der dritten und vierten Aussage kann man herleiten, dass gilt.
Danke für die Erklärungen zum Punkt und den Numeralen.--Schreiber 15:02, 1. Aug. 2012 (CEST)Beantworten
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:
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)Beantworten
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.
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)Beantworten

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

[Quelltext bearbeiten]

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)Beantworten

Konstruktion oder Überprüfung?

[Quelltext bearbeiten]

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 . (Um genau zu sein: die Formel ist , 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)Beantworten

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)Beantworten