Eine Variante eines Gödel-Satzes, konstruiert mit Rossers Trick, die die für Unvollständigkeit nötigen Hypothesen abschwächt: Sie liefert einen unentscheidbaren Satz für jede konsistente, rekursiv aufzählbare Theorie ohne die Forderung der ω-Konsistenz, indem sie ein modifiziertes Provabilitätsprädikat verwendet, das Beweisvergleiche einbezieht.

Prinzip

Rosser ersetzt das Standard-Provabilitätsprädikat durch eine Rosser-Provabilitätsrelation, die aussagt 'es gibt einen Beweis von mir und es gibt keinen kürzeren Beweis meiner Negation', oder verwendet äquivalent eine Zeugenordnung, um die stärkere Annahme der ω-Konsistenz im ursprünglichen Gödel-Argument zu vermeiden.

Demonstration

Für eine rekursiv axiomatisierbare T definiert man ein Rosser-artiges Prädikat RProv_T(x), das über kürzere Gegenbeweise quantifiziert, und wendet Diagonalisierung an, um einen Satz R mit T ⊢ (R ↔ ¬RProv_T(⌜R⌝)) zu erhalten. Ist T nur konsistent, zeigen Argumente über minimale Beweise, dass T weder R noch ¬R beweisen kann, sodass R in T unentscheidbar ist.

Fehlanwendung

Anzunehmen, Rosser-Sätze beseitigten alle metamathematischen Feinheiten: Sie schwächen die Hypothese von ω-Konsistenz auf bloße Konsistenz ab, benötigen aber weiterhin effektive Axiomatisierbarkeit und eine korrekte Formalisierung von Beweisvergleichen; sie machen Unvollständigkeitsargumente nicht trivial und beseitigen keine modelltheoretischen Unterschiede.

Konsequenz

Zeigt, dass Unvollständigkeit unter schwächeren Konsistenzhypothesen gilt und klärt die Rolle des Beweisvergleichs bei Unentscheidbarkeit; es verfeinert Gödels Ergebnis, indem es die Konsistenzanforderung für die Konstruktion unentscheidbarer Sätze herabsetzt.

Umkehrung

Beweist eine Theorie den Rosser-Satz oder dessen Negation, so liefert die in der Rosser-Konstruktion verwendete Beweisanalyse einen Widerspruch; damit zeigt die Beweisbarkeit von entweder dem Satz oder seiner Negation die Inkonsistenz unter den Annahmen der Konstruktion.

Abgrenzung

Gilt für rekursiv aufzählbare (effektiv axiomatisierte) Theorien, die Beweis- und Beweis-Längen-/Vergleichsbegriffe formal repräsentieren können; es gilt nicht für nicht-effektive Systeme oder Formalismen, die die erforderliche Ordnung der Beweise nicht darstellen können.

Semantische Spannung

Wettstreit mit dem Gödel-Satz durch Abwägung zwischen Hypothesenstärke und Einfachheit des Provabilitätsprädikats: Rosser-Sätze verwenden aufwändigere Beweisvergleichsmechanismen, um Unentscheidbarkeit unter schwächeren Annahmen zu erreichen und zeigen dadurch unterschiedliche technische Verhaltensweisen und metamathematische Deutungen.

Synthese

Ein Rosser-Satz ist ein arithmetisierter, selbstreferenzieller Satz, der mittels eines auf Beweisvergleichen empfindlichen Provabilitätsbegriffs konstruiert wird; durch Vermeidung der ω-Konsistenz zeigt er, dass bloße Konsistenz zusammen mit effektiver Axiomatisierbarkeit ausreicht, um unentscheidbare Sätze in formalen Theorien zu erzeugen.