Benutzer:Tino Cannst/Gödel-Rosser-Theorem

Dieser Artikel (Gödel-Rosser-Theorem) ist im Entstehen begriffen und noch nicht Bestandteil der freien Enzyklopädie Wikipedia.

Wenn du dies liest:

• Der Text kann teilweise in einer Fremdsprache verfasst, unvollständig sein oder noch ungeprüfte Aussagen enthalten.
• Wenn du Fragen zum Thema hast, nimm am besten Kontakt mit dem Autor Tino Cannst auf.

Wenn du diesen Artikel überarbeitest:

• Bitte denke daran, die Angaben im Artikel durch geeignete Quellen zu belegen und zu prüfen, ob er auch anderweitig den Richtlinien der Wikipedia entspricht (siehe Wikipedia:Artikel).
• Nach erfolgter Übersetzung kannst du diese Vorlage entfernen und den Artikel in den Artikelnamensraum verschieben. Die entstehende Weiterleitung kannst du schnelllöschen lassen.
• Importe inaktiver Accounts, die länger als drei Monate völlig unbearbeitet sind, werden gelöscht.

Vorlage:Importartikel/Wartung-2023-04

Das Gödel-Rosser-Theorem ist ein Satz der Mathematischen Logik zum Beweis von Gödelscher Unvollständigkeitssatz ohne die Annahme, dass die betrachtete Theorie ω-konsistent ist (Smorynski 1977, S. 840; Mendelson 1977, S. 160). Das Theorem wurde 1936 von J. Barkley Rosser als eine Verbesserung von Gödels ursprünglichem Beweis der Unvollständigkeitsatzes von 1931 veröffentlicht.

Während Gödels Originalbeweis einen Satz verwendet, der (informell) besagt: "Dieser Satz ist nicht beweisbar", beruht das Gödel-Rosser-Theorem auf einem Satz, der besagt: "Wenn dieser Satz beweisbar ist, gibt es einen kürzeren Beweis für seine Negation".

Hintergrund

Das Gödel-Rosser-Theorem beginnt mit den Annahmen des Gödelschen Unvollständigkeitssatzes. Es wird eine Theorie T gewählt, die wirksam und konsistent ist und ein hinreichendes Fragment der elementaren Arithmetik enthält.

Gödels Beweis zeigt, dass es für jede solche Theorie eine Formel Beweis T ( x , y ) {\displaystyle \operatorname {Proof} _{T}(x,y)} gibt, die die beabsichtigte Bedeutung hat, dass y y ein natürlicher Zahlencode (eine Gödel-Zahl) für eine Formel ist und x x die Gödel-Zahl für einen Beweis aus den Axiomen von T T der durch y y kodierten Formel ist. (Im weiteren Verlauf dieses Artikels wird nicht mehr zwischen der Zahl y y und der durch y y kodierten Formel unterschieden, und die Zahl, die eine Formel ϕ \phi kodiert, wird mit # ϕ {\displaystyle \#\phi } bezeichnet.) Außerdem wird die Formel Pvbl T ( y ) {\displaystyle \operatorname {Pvbl} _{T}(y)} definiert als ∃ x Proof T ( x , y ) {\displaystyle \exists x\operatorname {Proof} _{T}(x,y)}. Damit soll die Menge der aus T T beweisbaren Formeln definiert werden.

Die Annahmen über T T zeigen auch, dass es in der Lage ist, eine Negationsfunktion neg ( y ) {\displaystyle {\text{neg}}(y)} zu definieren, mit der Eigenschaft, dass wenn y y ein Code für eine Formel ϕ \phi ist, dann neg ( y ) {\displaystyle {\text{neg}}(y)} ein Code für die Formel ¬ ϕ \neg \phi ist. Die Negationsfunktion kann für Eingaben, die nicht Codes von Formeln sind, jeden beliebigen Wert annehmen.

Der Gödel-Satz der Theorie T T ist eine Formel ϕ \phi , manchmal als G T {\displaystyle G_{T}} bezeichnet, so dass T T beweist ϕ \phi ↔ ¬ Pvbl T ( # ϕ ) {\displaystyle \neg \operatorname {Pvbl} _{T}(\#\phi )}. Gödels Beweis zeigt, dass, wenn T T konsistent ist, der Gödel-Satz nicht bewiesen werden kann; aber um zu zeigen, dass auch die Negation des Gödel-Satzes nicht beweisbar ist, muss man eine stärkere Annahme hinzufügen, dass die Theorie ω-konsistent ist, nicht nur konsistent. Zum Beispiel beweist die Theorie T = PA + ¬ G P A {\displaystyle T={\text{PA}}+\neg {\text{G}}_{PA}}, in der PA Peano-Axiome sind, ¬ G T {\displaystyle \neg G_{T}}. Rosser (1936) konstruierte einen anderen selbstreferentiellen Satz, der verwendet werden kann, um den Gödel-Satz in Gödels Beweis zu ersetzen, wodurch die Notwendigkeit entfällt, ω-Konsistenz anzunehmen

Für eine feste arithmetische Theorie T T seien Proof T ( x , y ) {\displaystyle \operatorname {Proof} _{T}(x,y)} und neg ( x ) {\displaystyle {\text{neg}}(x)} das zugehörige Beweisprädikat und die Negationsfunktion.

Ein modifiziertes Beweisprädikat Proof T R ( x , y ) {\displaystyle \operatorname {Proof} _{T}^{R}(x,y)} ist definiert als:

Proof T R ( x , y ) ≡ Proof T ( x , y ) ∧ ¬ ∃ z ≤ x [ Proof T ( z , neg ( y ) ) ] , {\displaystyle \operatorname {Proof} _{T}^{R}(x,y)\equiv \operatorname {Proof} _{T}(x,y)\land \lnot \exists z\leq x[\operatorname {Proof} _{T}(z,\operatorname {neg} (y))],}

was bedeutet, dass

¬ Proof T R ( x , y ) ≡ Proof T ( x , y ) → ∃ z ≤ x [ Proof T ( z , neg ( y ) ) ] . {\displaystyle \lnot \operatorname {Proof} _{T}^{R}(x,y)\equiv \operatorname {Proof} _{T}(x,y)\zu \exists z\leq x[\operatorname {Proof} _{T}(z,\operatorname {neg} (y))].}

Dieses modifizierte Beweisprädikat wird verwendet, um ein modifiziertes Beweisbarkeitsprädikat Pvbl T R ( y ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(y)}:

Pvbl T R ( y ) ≡ ∃ x Beweis T R ( x , y ) . {\displaystyle \operatorname {Pvbl} _{T}^{R}(y)\equiv \exists x\operatorname {Proof} _{T}^{R}(x,y).}

Informell, Pvbl T R ( y ) {\displaystyle \operatorname {Pvbl} {\displaystyle \operatorname {Pvbl}(x,y)} ist die Behauptung, dass y y durch einen kodierten Beweis x x beweisbar ist, so dass es keinen kleineren kodierten Beweis für die Negation von y y y gibt. Unter der Annahme, dass T T konsistent ist, gilt für jede Formel ϕ \phi die Formel Pvbl T R ( # ϕ ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )} gilt dann und nur dann, wenn Pvbl T ( # ϕ ) {\displaystyle \operatorname {Pvbl} _{T}(\#\phi )} gilt, denn wenn es einen Code für den Beweis von ϕ \phi gibt, dann gibt es (gemäß der Konsistenz von T T) keinen Code für den Beweis von ¬ ϕ \neg \phi . Allerdings ist Pvbl T ( # ϕ ) {\displaystyle \operatorname {Pvbl} _{T}(\#\phi )} und Pvbl T R ( # ϕ ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )} haben unterschiedliche Eigenschaften unter dem Gesichtspunkt der Beweisbarkeit in T T.

Eine unmittelbare Folge der Definition ist, dass, wenn T T genügend Arithmetik enthält, dann kann man beweisen, dass für jede Formel ϕ \phi , Pvbl T R ( ϕ ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(\phi )} impliziert ¬ Pvbl T R ( neg ( ϕ ) ) {\displaystyle \neg \operatorname {Pvbl} _{T}^{R}({\text{neg}}(\phi ))}. Das liegt daran, dass es sonst zwei Zahlen n , m n,m gibt, die für die Beweise von ϕ \phi bzw. ¬ ϕ \neg \phi kodieren, die sowohl n < m n<m als auch m < n m<n erfüllen. (Tatsächlich braucht T T nur zu beweisen, dass eine solche Situation nicht für zwei beliebige Zahlen gelten kann, sowie einige Logik erster Ordnung einzubeziehen)

Unter Verwendung des Diagonal-Lemmas sei ρ \rho eine solche Formel, dass T T ρ ↔ ¬ PvblVorlage:Su(#ρ) beweist. ρ \rho ↔ ¬ Pvbl T ( # ρ ) {\displaystyle \neg \operatorname {Pvbl} _{T}(\#\rho )}. Die Formel ρ \rho ist der Rosser-Satz der Theorie T T. Rosser-Theorem

Sei T T eine effektive, konsistente Theorie mit einem hinreichenden Anteil an Arithmetik, mit dem Rosser-Satz $\rho$ . Dann gilt Folgendes (Mendelson 1977, S. 160):

   T T beweist nicht ρ \rho
   T T beweist nicht ¬ ρ \rho \displaystyle \neg \rho }

Um dies zu beweisen, zeigt man zunächst, dass für eine Formel y y und eine Zahl e e, wenn Proof T R ( e , y ) {\displaystyle \operatorname {Proof} _{T}^{R}(e,y)} gilt, dann beweist T T $ProofTR(e,y){\displaystyle \operatorname {Proof} _{T}^{R}(e,y)}$. Dies wird in ähnlicher Weise gezeigt, wie es in Gödels Beweis des ersten Unvollständigkeitssatzes geschieht: T T beweist Proof T ( e , y ) {\displaystyle \operatorname {Proof} _{T}(e,y)}, eine Relation zwischen zwei konkreten natürlichen Zahlen; man geht dann alle natürlichen Zahlen z z kleiner als e e einzeln durch, und für jedes z z beweist T T ¬ Proof T ( z , (neg ( y ) ) {\displaystyle \neg \operatorname {Proof} _{T}(z,{\text{(neg}}(y))}, wiederum eine Beziehung zwischen zwei konkreten Zahlen.

Die Annahme, dass T T genügend Arithmetik enthält (tatsächlich ist nur grundlegende Logik erster Ordnung erforderlich), stellt sicher, dass T T auch Pvbl T R ( y ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(y)} in diesem Fall beweist.

Außerdem, wenn T T konsistent ist und ϕ \phi beweist, dann gibt es eine Kodierung der Zahl e e für den Beweis in T T, und es gibt keine Kodierung der Zahl für den Beweis der Negation von ϕ \phi in T T. Daher gilt Proof T R ( e , y ) {\displaystyle \operatorname {Proof} _{T}^{R}(e,y)}, und somit beweist T T Pvbl T R ( # ϕ ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )}.

Der Beweis von (1) ist ähnlich wie in Gödels Beweis des ersten Unvollständigkeitssatzes: Nehmen wir an, T T beweist ρ \rho ; dann folgt aus der vorherigen Ausarbeitung, dass T T beweist Pvbl T R ( # ρ ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\rho )}. Somit beweist T T auch ¬ ρ {\displaystyle \neg \rho }. Aber wir haben angenommen, dass T T ρ \rho beweist, und das ist unmöglich, wenn T T konsistent ist. Wir sind gezwungen zu folgern, dass T T nicht ρ \rho beweist.

Der Beweis von (2) verwendet ebenfalls die besondere Form von $\operatorname {Proof} _{T}^{R}$. Nehmen wir an, $T$ beweist $\neg \rho$; dann folgt aus der vorherigen Ausarbeitung, dass $T$ $\operatorname {Pvbl} _{T}^{R}({\text{neg}}\#(\rho ))$ beweist. Aber durch die unmittelbare Konsequenz der Definition des Rosser'schen Beweisbarkeitsprädikats, die im vorherigen Abschnitt erwähnt wurde, folgt, dass $T$ $\neg \operatorname {Pvbl} _{T}^{R}(\#\rho )$ beweist. Somit beweist $T$ auch $\rho$. Aber wir haben angenommen, $T$ beweist $\neg \rho$, und das ist unmöglich, wenn $T$ konsistent ist. Wir sind gezwungen zu folgern, dass $T$ nicht $\neg \rho$ beweist.

References

• Mendelson (1977), Introduction to Mathematical Logic
• Smorynski (1977), "The incompleteness theorems", in Handbook of Mathematical Logic, Jon Barwise, Ed., North Holland, 1982, Vorlage:Isbn
• Barkley Rosser: Extensions of some theorems of Gödel and Church. In: Journal of Symbolic Logic. 1. Jahrgang, Nr. 3, September 1936, S. 87–91, doi:10.2307/2269028, JSTOR:2269028 (cambridge.org). 

Weblinks

• Avigad (2007), "Computability and Incompleteness", lecture notes.

[[Category:Mathematical logic]]