# 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 Σ 1 formula , and therefore from the Σ 1 completeness of Q it follows that each of its positive instances is provable. Here, Σ 1 -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.