Robinson arithmetic

The Robinson arithmetic (also: Q ) is a finite axiomatisiertes fragment of Peano arithmetic , a system of axioms of arithmetic , so the natural numbers , within the first predicate logic stage . It was introduced by Raphael Robinson in 1950 and essentially corresponds to Peano arithmetic without the axiom scheme of induction . The meaning of Robinson arithmetic comes from the fact that it is finitely axiomatizable, but cannot be completed recursively and is even essentially undecidable . This means that there is no consistent decidable extension of Robinson arithmetic. In particular, there is no complete recursively enumerable extension, since this would already be recursive (decidable).

Axioms

Robinson arithmetic is formulated in the first-order predicate logic with equality , represented by the predicate . Your language has the constant (called zero), the successor function (for successor : successor), which intuitively adds 1 to a given number, as well as the functions for addition and for multiplication. It has the following axioms, which formalize the elementary properties of natural numbers and arithmetic operations: ${\displaystyle =}$ ${\displaystyle \mathbf {0} }$ ${\displaystyle S}$ ${\displaystyle +}$ ${\displaystyle \times }$

• Zero has no predecessor: ${\displaystyle Sx\not =\mathbf {0} }$
• Different numbers have different successors: ${\displaystyle (Sx=Sy)\rightarrow x=y}$
• Every number is zero or has a predecessor: ${\displaystyle y=\mathbf {0} \vee \exists x(Sx=y)}$
• Recursive definition of addition and multiplication:
  • ${\displaystyle x+\mathbf {0} =x}$
  • ${\displaystyle x+Sy=S(x+y)}$
  • ${\displaystyle x\times \mathbf {0} =\mathbf {0} }$
  • ${\displaystyle x\times Sy=(x\times y)+x}$

Significance for Mathematical Logic

Robinson arithmetic plays a role especially in the proof of Gödel's first incompleteness theorem , since the relation “... is a proof of the formula ...” can be represented within Q and also in consistent axiomatic extensions of Q.

The representability of a predicate means that there is a formula so that the following applies to all natural numbers : ${\displaystyle P}$ ${\displaystyle \alpha =\alpha (x_{1},\ldots ,x_{n})}$ ${\displaystyle a_{1},\ldots ,a_{n}}$

(+) if the case is, then the statement in Q is provable, ${\displaystyle P(a_{1},\ldots ,a_{n})}$ ${\displaystyle \alpha ({\underline {a_{1}}},\ldots ,{\underline {a_{n}}})}$

(-) if not true, then the statement in Q is provable. ${\displaystyle P(a_{1},\ldots ,a_{n})}$ ${\displaystyle \neg \alpha ({\underline {a_{1}}},\ldots ,{\underline {a_{n}}})}$

The term is defined as follows: ${\displaystyle {\underline {a}}}$

${\displaystyle {\underline {0}}=\mathbf {0} }$,

${\displaystyle {\underline {n+1}}=S{\underline {n}}}$.

The associated provability predicate "... is provable" (i.e. "there is one that is a proof of the formula ...") cannot be represented in Q because none of its negative instances ("the formula ... is not provable") in Q can be proven. However, it can be expressed by a Σ ₁ formula , and therefore from the Σ ₁ completeness of Q it follows that each of its positive instances is provable. Here, Σ ₁ -completeness is understood to mean that every Σ _1- statement (the language of Q ) that applies to the natural numbers can also be proven in Q. ${\displaystyle b}$

Q can already be interpreted in relatively weak sub-theories of ZFC , for example in the so-called Tarski fragment TF, which only consists of the following three axioms: the axiom of extensionality (also the axiom of determination), the axiom of empty sets (also the axiom of zero sets: the empty set exists) and the axiom which, for two sets , requires the existence of the adjoint set . ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle x\cup \{y\}}$

literature

• A. Bezboruah, John C. Shepherdson: Godel's incompleteness theorem Second Q for . In: Journal of Symbolic Logic . tape 41 , no. 2 , 1976, p. 503-512 , JSTOR : 2272251 .
• George S. Boolos , John P. Burgess, Richard C. Jeffrey: Computability and Logic . 5th edition. Cambridge University Press, Cambridge etc. 2007.
• Petr Hájek, Pavel Pudlák: Metamathematics of first-order arithmetic . 2nd Edition. Springer-Verlag, 1998.
• Raphael Robinson : An Essentially Undecidable Axiom System . In: Proceedings of the International Congress of Mathematics . 1950, p. 729-730 .
• Alfred Tarski , Andrzej Mostowski , Raphael Robinson : Undecidable theories . North Holland, 1953.
• Hans Hermes : Introduction to Mathematical Logic . 2nd Edition. BG Teubner Stuttgart, 1969.
• Wolfgang Rautenberg : Introduction to Mathematical Logic . 3. Edition. Vieweg + Teubner, Wiesbaden 2008, ISBN 978-3-8348-0578-2 , doi : 10.1007 / 978-3-8348-9530-1 .
• Donald Monk: Mathematical Logic (=  Graduate Texts in Mathematics . Volume 37 ). Springer, New York 1976, ISBN 0-387-90170-1 .

Individual evidence

1. ↑ Rautenberg (2008), sentence 6.4.4, p. 191
2. ↑ George Boolos , John P. Burgess, Richard Jeffrey: Computability and Logic . 4th edition. Cambridge University Press, 2002, ISBN 0-521-70146-5 , pp. 56 .
3. ^ W. Rautenberg (2008), p. 186.
4. ^ W. Rautenberg (2008), p. 184.
5. ^ W. Rautenberg (2008), p. 83.
6. ^ W. Rautenberg (2008), p. 190.
7. ^ W. Rautenberg (2008), p. 186.
8. ↑ D. Monk (1976), pp. 283-290.