nLab Robinson arithmetic

Robinson arithmetic


Model theory


Robinson arithmetic


Robinson arithmetic (after Raphael M. Robinson) is a finitely axiomatized weakening of Peano arithmetic in which the induction schema is dropped and minimal axioms remain.


Robinson arithmetic, also denoted by Q, is a first-order theory whose signature is that of first-order Peano arithmetic: it consists of a constant 00, an unary function symbol ss, and binary function symbols +,+, \cdot. The axioms are

  1. x¬s(x)=0\forall_x \neg s(x) = 0;

  2. x,ys(x)=s(y)x=y\forall_{x, y} s(x) = s(y) \Rightarrow x = y;

  3. xx=0 yx=s(y)\forall_x x = 0 \vee \exists_y x = s(y);

  4. xx+0=x\forall_x x + 0 = x,

  5. x,yx+s(y)=s(x+y)\forall_{x, y} x + s(y) = s(x+y);

  6. xx0=0\forall_x x \cdot 0 = 0;

  7. x,yxs(y)=xy+x\forall_{x, y} x \cdot s(y) = x \cdot y + x.

There is no induction scheme.

One sometimes adds axioms for order; however, this is also definable. (Citation in Wikipedia; I can't quite make it work.)

Category of models of Robinson arithmetic

A model of Robinson arithmetic is a set NN with an element 0N0 \in N, a function s:NNs:N \to N, and binary operations ()+():N×NN(-)+(-):N \times N \to N and ()():N×NN(-)\cdot(-):N \times N \to N, such that

  • for all xNx \in N, ¬s(x)=0\neg s(x) = 0

  • for all x,yNx, y \in N, s(x)=s(y)s(x) = s(y) implies x=yx = y

  • for all xNx \in N, x=0x = 0 or there exists yNy \in N where x=s(y)x = s(y)

  • for all xNx \in N, x+0=xx + 0 = x

  • for all x,yNx, y \in N, x+s(y)=s(x+y)x + s(y) = s(x+y)

  • for all xNx \in N, x0=0x \cdot 0 = 0

  • for all x,yNx, y \in N, xs(y)=xy+xx \cdot s(y) = x \cdot y + x

A homomorphism of models of Robinson arithmetic NN and N N^{'} is a function f:NN f:N \to N^{'} such that

  • f(0 N)=0 N f(0_N) = 0_{N^{'}}

  • for all xNx \in N, f(s N(x))=s N (f(x))f(s_N(x)) = s_{N^{'}}(f(x))

  • for all x,yNx, y \in N, f(x+ Ny)=f(x)+ N f(y)f(x +_N y) = f(x) +_{N^{'}} f(y)

  • for all x,yNx, y \in N, f(x Ny)=f(x) N f(y)f(x \cdot_N y) = f(x) \cdot_{N^{'}} f(y)

The category of models of Robinson arithmetic in a universe 𝒰\mathcal{U} is the category

RobinsonArithmetics 𝒰\mathrm{RobinsonArithmetics}_\mathcal{U}

whose objects

Ob(RobinsonArithmetics 𝒰)Ob(\mathrm{RobinsonArithmetics}_\mathcal{U})

are the models of Nelson arithmetic, and for any two objects

AOb(RobinsonArithmetics 𝒰)A \in Ob(\mathrm{RobinsonArithmetics}_\mathcal{U})


BOb(RobinsonArithmetics 𝒰)B \in Ob(\mathrm{RobinsonArithmetics}_\mathcal{U})

the morphisms

Mor RobinsonArithmetics 𝒰(A,B)Mor_{\mathrm{RobinsonArithmetics}_\mathcal{U}}(A, B)

are the homomorphisms of models of Nelson arithmetic as defined above.

This category is an accessible category. If 𝒰\mathcal{U} satisfies the axiom of finiteness, then the category RobinsonArithmetics 𝒰\mathrm{RobinsonArithmetics}_\mathcal{U} has no initial object and is an empty category.


Despite the considerable weakening of what can be proved, the formulas are the same as in Peano arithmetic, and all the background number theory (the Chinese remainder theorem? and the like) needed to develop Gödel codings, incompleteness theorems, and so on is still there. In some sense the axioms are a minimal set needed to carry out this program (and in fact this was in large part the motivation for Robinson).


Unlike the case for Peano arithmetic, system QQ admits tractable computable nonstandard? models.

The simplest consists of a single nonstandard number \infty (in addition to all of the standard numbers, which exist in every model), with the rules (where nn is a standard number):

  • s()=s(\infty) = \infty,
  • n+,+n,+=n + \infty, \infty + n, \infty + \infty = \infty,
  • 0,0=00 \cdot \infty, \infty \cdot 0 = 0, s(n),s(n),=s(n) \cdot \infty, \infty \cdot s(n), \infty \cdot \infty = \infty.

See also


Last revised on May 10, 2022 at 01:48:27. See the history of this page for a list of all contributions to it.