On a Theorem by Bezboruah & Shepherdson

Der Artikel verteidigt den Unvollständigkeitssatz von Bezboruah und Shepherdson gegen Kreisels Kritik, vergleicht ihn mit Pudláks Erweiterung des zweiten Unvollständigkeitssatzes und liefert einen neuen Beweis des Satzes unter Verwendung einer Sequenzkodierung nach Nielsen und Markov.

Das Wesentliche

Hier ist eine Erklärung des wissenschaftlichen Artikels von Albert Visser, übersetzt in eine einfache, bildhafte Sprache für ein allgemeines Publikum.

Der große Streit um die „Unvollständigkeit"

Stellen Sie sich vor, die Mathematik ist ein riesiges Schloss, und die Logiker sind die Architekten, die versuchen, die Sicherheitstüren zu verstehen. Eine dieser Türen ist das berühmte Gödel'sche Unvollständigkeitstheorem. Gödel hat gezeigt, dass es in jedem komplexen enoughen mathematischen System eine Aussage gibt, die man weder beweisen noch widerlegen kann – und zwar genau dann, wenn das System konsistent (widerspruchsfrei) ist. Kurz gesagt: Ein System kann seine eigene Unfehlbarkeit nicht beweisen.

Doch dann gab es einen kleinen, aber feinen Streit unter den Architekten.

1. Der Konflikt: Ist das Tor wirklich ein Tor?

In den 1970er Jahren haben zwei Architekten, Bezboruah und Shepherdson, behauptet, dass dieses Theorem sogar für ein sehr kleines, schwaches mathematisches System gilt, das nur die Grundlagen der Arithmetik (Zahlenlehre) kennt. Sie sagten: „Selbst dieses kleine System kann nicht beweisen, dass es keine Widersprüche enthält."

Doch ein sehr einflussreicher Architekt namens Georg Kreisel warf einen Eimer kaltes Wasser darauf. Kreisel sagte: „Wartet mal! Ihr behauptet, das System könne seine eigene Sicherheit nicht beweisen. Aber das System ist so dumm und schwach, dass es gar nicht versteht, was 'Sicherheit' bedeutet! Es kann nicht einmal die einfachsten Regeln der Addition beweisen. Wenn ihr sagt, es beweise seine eigene Unvollständigkeit, dann ist das wie wenn ein Kleinkind behauptet, es könne die Gesetze der Physik nicht verstehen. Das ist bedeutungslos."

Kreisel meinte also: Die Aussage „Ich bin sicher" ist in diesem kleinen System nur ein leeres Wortgeplänkel, kein echtes mathematisches Konzept.

2. Visser nimmt das Wort: „Kreisel hat unrecht!"

Der Autor dieses Artikels, Albert Visser, sagt: „Nein, Kreisel irrt sich."
Visser benutzt eine schöne Analogie: Stellen Sie sich vor, Sie haben einen Satz, der in der komplexen Welt der ZFC-Mathematik (dem „großen Schloss") bewiesen wurde. Wenn Sie nun fragen: „Können wir das auch ohne die Auswahlaxiome beweisen?", ist die Antwort „Nein". Aber das bedeutet nicht, dass der Satz im kleinen System eine andere Bedeutung hat. Er hat immer noch dieselbe Bedeutung, nur dass das kleine System zu schwach ist, ihn zu beweisen.

Visser argumentiert, dass wir die Frage nicht dadurch abtun können, dass wir sagen, das kleine System habe eine andere Sprache. Die Frage, ob ein System seine eigene Konsistenz beweisen kann, ist auch für schwache Systeme spannend und technisch herausfordernd.

3. Der Vergleich: Der alte Weg vs. der neue Weg

Visser vergleicht die Arbeit von Bezboruah und Shepherdson mit einer modernen Methode, die von einem anderen Architekten, Pavel Pudlák, entwickelt wurde.

• Der moderne Weg (Pudlák): Das ist wie ein hochmodernes, automatisiertes Sicherheitssystem. Es nutzt komplexe Interpretationen und funktioniert für fast alle Systeme, ist aber technisch sehr anspruchsvoll und schwer zu durchschauen.
• Der alte Weg (Bezboruah & Shepherdson): Das ist wie ein handgefertigter, mechanischer Trick. Es ist spezifisch, nutzt eine sehr spezielle Art, Zahlen und Beweise zu kodieren (wie ein spezieller Code), und ist viel einfacher zu verstehen. Man kann sich den Beweis fast wie ein mechanisches Puzzle vorstellen, bei dem man zeigt, wie man in einem kleinen System einen scheinbaren Widerspruch konstruiert.

Visser zeigt, dass beide Wege zum selben Ergebnis führen (das kleine System kann seine Sicherheit nicht beweisen), aber sie sind völlig unterschiedliche Methoden. Der alte Weg ist didaktisch wertvoll, weil man genau sieht, wie der Beweis funktioniert, ohne in die tiefen Abgründe der modernen Logik abtauchen zu müssen.

4. Der neue Beweis: Der „Markov-Code"

Im letzten Teil des Artikels macht Visser etwas Kreatives. Er nimmt die Idee von Bezboruah und Shepherdson und verbessert sie mit einer neuen Methode, die auf Markov-Codierung basiert.

Stellen Sie sich vor, man muss eine lange Kette von Anweisungen (einen Beweis) in einem System speichern, das nur sehr einfache Werkzeuge hat.

• Die alte Methode (β-Funktion): Das ist wie das Speichern einer Kette in einem alten, komplizierten Schrank.
• Die neue Methode (Markov): Visser nutzt eine Idee, die auf Matrizen (Zahlenblöcken) basiert. Er stellt sich vor, dass jede Zahl oder jeder Schritt in einem Beweis eine spezielle Art von „Baustein" ist. Diese Bausteine können wie Legosteine zusammengefügt werden.

Er konstruiert eine fiktive Welt (ein mathematisches Modell), in der diese Bausteine so angeordnet sind, dass sie am Anfang wie harmlose, wahre Sätze aussehen, aber am Ende plötzlich einen Widerspruch ergeben. Es ist, als würde man eine Kette von Ziegelsteinen bauen, die am Anfang stabil wirkt, aber durch eine geschickte Anordnung am Ende zusammenbricht – und das System selbst kann diesen Zusammenbruch nicht verhindern, weil es die Regeln für das Zusammenbauen nicht vollständig versteht.

Fazit: Warum ist das wichtig?

Visser sagt im Grunde:

1. Kreisel hatte Unrecht: Auch schwache Systeme haben eine Bedeutung, und die Frage nach ihrer Konsistenz ist wichtig.
2. Die alte Methode ist Gold wert: Der Beweis von Bezboruah und Shepherdson ist nicht veraltet. Er ist ein wunderbares Werkzeug, um zu verstehen, wie Logik funktioniert, weil er so konkret und „sichtbar" ist.
3. Neue Tricks: Mit der neuen Markov-Methode kann man diesen Beweis noch eleganter und verständlicher machen.

Es ist wie bei einem alten, handgefertigten Uhrwerk: Auch wenn es moderne, digitale Uhren gibt, ist es faszinierend zu sehen, wie die alten Räder ineinandergreifen, um die Zeit zu messen. Visser zeigt uns, wie diese alten Räder (der Beweis) funktionieren und warum sie immer noch funktionieren.

Technische Zusammenfassung

Hier ist eine detaillierte technische Zusammenfassung des Artikels „On a Theorem by Bezboruah & Shepherdson" von Albert Visser auf Deutsch.

1. Problemstellung und Hintergrund

Der Artikel befasst sich mit einem spezifischen Ergebnis zur Unvollständigkeit, das 1976 von Amala Bezboruah und John C. Shepherdson in ihrer Arbeit [BS76] bewiesen wurde. Das Kernresultat besagt, dass die schwache arithmetische Theorie $PA^-$ (die Theorie des nicht-negativen Teils eines diskret geordneten kommutativen Rings) die Konsistenz einer extrem schwachen Theorie (genannt BeSh) nicht beweisen kann. Daraus folgt, dass auch schwächere Theorien wie Robinsons Q oder R ihre eigene Konsistenz nicht beweisen können.

Das zentrale Problem, das Visser adressiert, ist die philosophische und methodische Kritik von Georg Kreisel an diesem Ergebnis. Kreisel argumentierte, dass in so schwachen Systemen wie $Q$ oder $PA^-$ die üblichen Formeln, die Konsistenz ausdrücken sollen (z. B. $\text{con}(Q)$), nicht als echte Ausdrucke der Konsistenz interpretiert werden können. Seine Begründung: Diese Systeme können die notwendigen Eigenschaften des Beweisprädikats (die Hilbert-Bernays- oder Löb-Bedingungen) nicht formal verifizieren. Für Kreisel sei die Aussage daher nur eine algebraische Eigenschaft ohne philosophische Bedeutung.

Visser stellt sich die Aufgabe, diese Kritik zu widerlegen, den Satz von Bezboruah-Shepherdson (B-S) mit modernen Ergebnissen (insbesondere von Pavel Pudlák) zu vergleichen und einen neuen, unabhängigen Beweis für den B-S-Satz zu liefern, der auf einer anderen Kodierungstechnik basiert.

2. Methodik

Visser verfolgt einen dreifachen methodischen Ansatz:

1. Philosophische Analyse und Widerlegung der Kreisel-Kritik:
   Visser argumentiert, dass Kreisels Forderung, ein System müsse die Löb-Bedingungen intern beweisen können, um als „sinnvoll" zu gelten, unbegründet ist. Er plädiert dafür, die Bedeutung von Formeln durch die Semantik der natürlichen Zahlen (die intendierte Interpretation) festzulegen, nicht durch die Beweiskraft des schwachen Subsystems selbst. Selbst wenn man Inferenzialist ist, ändert sich die Bedeutung einer Aussage nicht dadurch, dass ein schwächeres System sie nicht beweisen kann.

2. Vergleich mit modernen Inkomplettheits-Sätzen (Pudlák):
   Der Autor vergleicht das B-S-Ergebnis mit Pavel Pudláks Erweiterung des zweiten Unvollständigkeitssatzes. Pudlák zeigte, dass $Q$ einen definierbaren Schnitt (cut) interpretiert, auf dem die Theorie $S^1_2$ (eine Theorie für polynomielle Zeitberechenbarkeit) lebt. Da $S^1_2$ den zweiten Unvollständigkeitssatz erfüllt, folgt daraus, dass $Q$ die Konsistenz von $Q$ nicht beweisen kann. Visser hebt die Unterschiede hervor: Der Pudlák-Ansatz ist interpretationsbasiert und gilt für eine breite Klasse von Kodierungen, während der B-S-Ansatz konstruktiv ist und spezifische Kodierungen (wie die $\beta$-Funktion) erfordert.

3. Neubeweis mittels Markov-Kodierung:
   Der Hauptteil des Artikels (Abschnitt 4) liefert einen neuen Beweis des B-S-Theorems. Anstatt der klassischen $\beta$-Funktion (die in [BS76] verwendet wurde), nutzt Visser eine Kodierung von Folgen, die auf der Struktur der Gruppe $SL_2(\mathbb{Z}^+)$ (die Gruppe der $2 \times 2$-Matrizen mit ganzzahligen Einträgen und Determinante 1, mit nicht-negativen Einträgen) basiert.

   • Grundidee: $SL_2(\mathbb{Z}^+)$ ist isomorph zur freien Monoid auf zwei Erzeugern $A$ und $B$. Folgen können als Produkte von Matrizen kodiert werden.
   • Konstruktion des Modells: Visser konstruiert ein Modell $K$ von $PA^-$, das alle wahren universellen Sätze erfüllt. Dazu verwendet er nicht-standard Modelle der wahren Arithmetik ($M$ und $N$, wobei $N$ eine elementare End-Erweiterung von $M$ ist).
   • Der Trick: Er definiert eine Matrix $\beta = [n]^a [m]^b$, wobei $a \in M$ und $b \in N \setminus M$ nicht-standard Elemente sind. In $N$ ist $\beta$ keine gültige Beweisfolge. Durch die Konstruktion eines Teilmodells $K$ (basierend auf den Ringoperationen der Einträge von $\beta$) wird erreicht, dass $\beta$ in $K$ existiert, aber der „Übergang" von den Axiomen zu den Schlussfolgerungen (der Punkt, an dem die Beweisstruktur zusammenbricht) nicht mehr sichtbar ist. In $K$ erscheint $\beta$ somit als ein gültiger Beweis für einen Widerspruch ($\bot$).

3. Wichtige Beiträge und Ergebnisse

• Verteidigung des B-S-Theorems: Visser zeigt, dass Kreisels Einwand nicht haltbar ist. Die Frage, ob schwache Theorien ihre Konsistenz beweisen können, ist technisch und philosophisch relevant, auch wenn die internen Beweiseigenschaften des Beweisprädikats schwach sind.
• Klarstellung der Beziehung zu Pudlák: Der Artikel differenziert präzise zwischen dem „Gödel-Pudlák"-Ansatz (interpretationsbasiert, robust gegenüber Kodierungsvariationen, nutzt Löb-Regel) und dem „Bezboruah-Shepherdson"-Ansatz (konstruktiv, modelltheoretisch, spezifisch für bestimmte Kodierungen und Hilbert-Systeme). Beide Ergebnisse sind unterschiedlich, überschneiden sich aber im Ergebnis für $Q$.
• Neuer Beweis durch Markov-Kodierung: Visser liefert einen vollständigen, alternativen Beweis für das B-S-Theorem.
  • Er nutzt die Eigenschaften der Matrizen $[n] = \begin{pmatrix} 1 & n \\ 0 & 1 \end{pmatrix}$ und die damit verbundenen rekursiven Folgen $s_{n,m}$.
  • Er beweist ein zentrales Lemma (Lemma 4.3), dass ein bestimmtes Element $x_1$ (das für die Länge der Axiom-Sequenz steht) nicht im konstruierten Ring $K_0$ liegt, obwohl die Matrix $\beta$, die die Sequenz repräsentiert, in $K$ liegt. Dies führt dazu, dass die Sequenz in $K$ als Beweis für $\bot$ interpretiert wird, obwohl sie es in der Standardarithmetik nicht ist.
• Didaktischer Wert: Die Konstruktion liefert ein konkretes, rekursives Modell, in dem ein Inkonsistenzbeweis „sichtbar" ist, was im Gegensatz zu Modellen schwacher Theorien wie $S^1_2$ steht, wo solche Beweise oft nicht visualisierbar sind.

4. Signifikanz

Der Artikel hat mehrere wichtige Implikationen für die mathematische Logik:

1. Wiederbelebung eines vernachlässigten Ergebnisses: Das B-S-Theorem wurde oft aufgrund Kreisels Kritik ignoriert. Visser rehabilitiert es als ein tiefgründiges technisches Ergebnis, das die Grenzen der Beweisbarkeit in schwachen Systemen aufzeigt.
2. Methodische Vielfalt: Durch die Einführung der Markov-Kodierung (basierend auf $SL_2$) zeigt Visser, dass das B-S-Ergebnis nicht an die $\beta$-Funktion gebunden ist. Dies erweitert den Anwendungsbereich und die Robustheit des Theorems.
3. Klärung der „Intensionalität": Der Beitrag trägt zur Debatte bei, was es bedeutet, dass eine Formel „Konsistenz ausdrückt". Visser argumentiert, dass dies primär eine Frage der Semantik (der Standardmodelle) ist und nicht davon abhängt, ob das schwache System selbst die Eigenschaften des Beweisprädikats beweisen kann.
4. Offene Fragen: Der Artikel wirft neue Fragen auf, z. B. ob das von Bezboruah und Shepherdson konstruierte Modell alle wahren universellen Sätze erfüllt (Open Question 3.6) und wie sich die Konstruktion auf andere Beweissysteme (wie den Gentzen-Kalkül) übertragen lässt.

Zusammenfassend stellt Visser sicher, dass das Theorem von Bezboruah und Shepherdson als ein eigenständiges, wichtiges Ergebnis der Beweistheorie anerkannt wird, das komplementär zu den modernen, interpretationsbasierten Sätzen von Pudlák steht, und liefert zudem einen eleganten neuen Beweis, der auf algebraischen Strukturen basiert.