Robinson-Arithmetik

Die Robinson-Arithmetik (auch: Q) ist ein endlich axiomatisiertes Fragment der Peano-Arithmetik, eines Axiomensystems der Arithmetik, also der natürlichen Zahlen, innerhalb der Prädikatenlogik erster Stufe. Sie wurde 1950 von Raphael Robinson eingeführt und entspricht im Wesentlichen der Peano-Arithmetik ohne das Axiomenschema der Induktion. Die Bedeutung der Robinson-Arithmetik rührt daher, dass sie endlich axiomatisierbar, aber nicht rekursiv vervollständigbar ist und sogar wesentlich unentscheidbar ist. Dies bedeutet, dass es keine konsistente entscheidbare Erweiterung der Robinson-Arithmetik gibt. Es gibt damit insbesondere auch keine vollständige rekursiv aufzählbare Erweiterung, da diese bereits rekursiv (entscheidbar) wäre.<ref>Rautenberg (2008), Satz 6.4.4, S. 191</ref>

Axiome

Die Robinson-Arithmetik ist formuliert in der Prädikatenlogik erster Stufe mit Gleichheit, repräsentiert durch das Prädikat <math>=</math>. Ihre Sprache hat die Konstante <math>\mathbf{0}</math> (genannt Null), die Nachfolgerfunktion <math>S</math> (für successor: Nachfolger), welche intuitiv zu einer gegebenen Zahl 1 addiert, sowie die Funktionen <math>+</math> für Addition und <math>\times</math> für Multiplikation. Sie hat folgende Axiome, die elementare Eigenschaften der natürlichen Zahlen und der arithmetischen Operationen formalisieren:<ref>{{#invoke:Vorlage:Literatur|f}}</ref>

Null hat keinen Vorgänger: <math>Sx\not= \mathbf{0}</math>
Verschiedene Zahlen haben verschiedene Nachfolger: <math>(Sx = Sy) \rightarrow x=y</math>
Jede Zahl ist gleich Null oder hat einen Vorgänger: <math>y=\mathbf{0} \vee \exists x(Sx=y)</math>
Rekursive Definition von Addition und Multiplikation:
- <math>x+\mathbf{0} = x</math>
- <math>x+Sy = S(x+y)</math>
- <math>x\times \mathbf{0} = \mathbf{0}</math>
- <math>x\times Sy = (x\times y)+x</math>

Bedeutsamkeit für die Mathematische Logik

Die Robinson-Arithmetik spielt insbesondere beim Beweis des ersten Gödelschen Unvollständigkeitssatzes eine Rolle, da sich innerhalb von Q und ebenso in konsistenten axiomatischen Erweiterungen von Q die Beziehung „… ist ein Beweis der Formel …“ repräsentieren lässt.<ref>W. Rautenberg (2008), S. 186.</ref>

Dabei bedeutet Repräsentierbarkeit eines Prädikats <math>P</math>, dass es eine Formel <math>\alpha = \alpha(x_1,\ldots, x_n)</math> gibt, so dass für alle natürlichen Zahlen <math>a_1,\ldots ,a_n</math> gilt:

(+) falls <math>P(a_1,\ldots ,a_n)</math> der Fall ist, dann ist die Aussage <math>\alpha (\underline{a_1},\ldots, \underline{a_n})</math> in Q beweisbar,

(-) falls <math>P(a_1,\ldots ,a_n)</math> nicht zutrifft, dann ist die Aussage <math>\neg \alpha (\underline{a_1},\ldots, \underline{a_n})</math> in Q beweisbar.<ref>W. Rautenberg (2008), S. 184.</ref>

Der Term <math>\underline{a}</math> ist dabei wie folgt definiert:

<math> \underline{0} = \mathbf{0}</math>,

<math> \underline{n+1} = S\underline{n}</math>.<ref>W. Rautenberg (2008), S. 83.</ref>

Das zugehörige Beweisbarkeitsprädikat „… ist beweisbar“ (d. h. „es gibt ein <math>b</math>, das ein Beweis der Formel … ist“) ist nicht in Q repräsentierbar, weil keine seiner negativen Instanzen („die Formel … ist nicht beweisbar“) in Q beweisbar ist. Es kann jedoch durch eine Σ₁-Formel ausgedrückt werden, und daher folgt aus der Σ₁-Vollständigkeit von Q,<ref>W. Rautenberg (2008), S. 190.</ref> dass jede seiner positiven Instanzen beweisbar ist. Unter Σ₁-Vollständigkeit ist hier zu verstehen, dass jede Σ₁-Aussage (der Sprache von Q), die für die natürlichen Zahlen gilt, auch in Q beweisbar ist.<ref>W. Rautenberg (2008), S. 186.</ref>

Q ist bereits in relativ schwachen Subtheorien von ZFC interpretierbar, etwa im sogenannten Tarski-Fragment TF,<ref>D. Monk (1976), S. 283–290.</ref> das nur aus folgenden drei Axiomen besteht: dem Extensionalitätsaxiom (auch Axiom der Bestimmtheit), dem Leermengenaxiom (auch Nullmengenaxiom: die leere Menge existiert) und dem Axiom, welches für zwei Mengen <math>x</math>, <math>y</math> die Existenz der adjungierten Menge <math>x \cup \{y\}</math> fordert.

Literatur

{{#invoke:Vorlage:Literatur|f}}
{{#invoke:Vorlage:Literatur|f}}
{{#invoke:Vorlage:Literatur|f}}
{{#invoke:Vorlage:Literatur|f}}
{{#invoke:Vorlage:Literatur|f}}
{{#invoke:Vorlage:Literatur|f}}
{{#invoke:Vorlage:Literatur|f}}
{{#invoke:Vorlage:Literatur|f}}

Einzelnachweise