Robinson arithmetic (source code)

= Robinson arithmetic
{c}
{title2=$\mathsf Q$}
{wiki}

<Robinson arithmetic> is a finitely axiomatized <first-order theory> in the language $0,S,+,\cdot$. Its seven axioms are the universal closures of
$$
Sx\ne0,\quad Sx=Sy\Rightarrow x=y,\quad x\ne0\Rightarrow\exists y\ x=Sy,
$$
$$
x+0=x,\quad x+Sy=S(x+y),\quad x\cdot0=0,\quad x\cdot Sy=x\cdot y+x.
$$
They describe successor, addition and multiplication without an induction schema. Each calculation on particular standard <numerals> can still be verified: repeated use of the recursion equations proves, for example, $\overline2+\overline3=\overline5$. This finite computational strength is enough for representing computable finite calculations and for the <diagonal lemma> used in <crude incompleteness theorem>. <Peano arithmetic> adds induction for arbitrary arithmetic formulas.<Introduction to the Theory of Computation: Computability, Complexity, and the Lambda Calculus by Jean Gallier and Jocelyn Quaintance (2020)>[Chapter6, printed p.156, seven axioms and induction schema]{ref}