Primitive recursive arithmetic

Primitive recursive arithmetic (PRA) is a

• A
  countably infinite
  number of variables x, y, z,....
• The propositional connectives;
• The equality symbol =, the constant symbol 0, and the successor symbol S (meaning add one);
• A symbol for each primitive recursive function.

The logical axioms of PRA are the:

• Tautologies of the propositional calculus;
• Usual axiomatization of equality as an equivalence relation.

The logical rules of PRA are modus ponens and variable substitution.
The non-logical axioms are, firstly:

• ${\displaystyle S(x)\neq 0}$;
• ${\displaystyle S(x)=S(y)\to x=y,}$

where ${\displaystyle x\neq y}$ always denotes the negation of ${\displaystyle x=y}$ so that, for example, ${\displaystyle S(0)=0}$ is a negated proposition.

Further, recursive defining equations for every primitive recursive function may be adopted as axioms as desired. For instance, the most common characterization of the primitive recursive functions is as the 0 constant and successor function closed under projection, composition and primitive recursion. So for a (n+1)-place function f defined by primitive recursion over a n-place base function g and (n+2)-place iteration function h there would be the defining equations:

• ${\displaystyle f(0,y_{1},\ldots ,y_{n})=g(y_{1},\ldots ,y_{n})}$
• ${\displaystyle f(S(x),y_{1},\ldots ,y_{n})=h(x,f(x,y_{1},\ldots ,y_{n}),y_{1},\ldots ,y_{n})}$

Especially:

• ${\displaystyle x+0=x\ }$
• ${\displaystyle x+S(y)=S(x+y)\ }$
• ${\displaystyle x\cdot 0=0\ }$
• ${\displaystyle x\cdot S(y)=x\cdot y+x\ }$
• ... and so on.

PRA replaces the

• From ${\displaystyle \varphi (0)}$ and ${\displaystyle \varphi (x)\to \varphi (S(x))}$, deduce ${\displaystyle \varphi (y)}$, for any predicate ${\displaystyle \varphi .}$

In

It is possible to formalise PRA in such a way that it has no logical connectives at all—a sentence of PRA is just an equation between two terms. In this setting a term is a primitive recursive function of zero or more variables. Curry (1941) gave the first such system. The rule of induction in Curry's system was unusual. A later refinement was given by Goodstein (1954). The rule of induction in Goodstein's system is:

${\displaystyle {F(0)=G(0)\quad F(S(x))=H(x,F(x))\quad G(S(x))=H(x,G(x)) \over F(x)=G(x)}.}$

Here x is a variable, S is the successor operation, and F, G, and H are any primitive recursive functions which may have parameters other than the ones shown. The only other

${\displaystyle {F(x)=G(x) \over F(A)=G(A)}\qquad {A=B \over F(A)=F(B)}\qquad {A=B\quad A=C \over B=C}.}$

Here A, B, and C are any terms (primitive recursive functions of zero or more variables). Finally, there are symbols for any primitive recursive functions with corresponding defining equations, as in Skolem's system above.

In this way the propositional calculus can be discarded entirely. Logical operators can be expressed entirely arithmetically, for instance, the absolute value of the difference of two numbers can be defined by primitive recursion:

${\displaystyle {\begin{aligned}P(0)=0\quad &\quad P(S(x))=x\\x{\dot {-}}0=x\quad &\quad x{\mathrel {\dot {-}}}S(y)=P(x{\mathrel {\dot {-}}}y)\\|x-y|=&(x{\mathrel {\dot {-}}}y)+(y{\mathrel {\dot {-}}}x).\\\end{aligned}}}$

Thus, the equations x=y and ${\displaystyle |x-y|=0}$ are equivalent. Therefore, the equations ${\displaystyle |x-y|+|u-v|=0}$ and ${\displaystyle |x-y|\cdot |u-v|=0}$ express the logical

can be expressed as ${\displaystyle 1{\dot {-}}|x-y|=0}$.

See also

• Elementary recursive arithmetic
• Finite-valued logic
• Heyting arithmetic
• Peano arithmetic
• Primitive recursive function
• Robinson arithmetic
• Second-order arithmetic
• Skolem arithmetic

• MR 0004207
  .

• MR 0087614
  .

• MR 0209111
  .

• MR 0124194
  .

• Skolem, Thoralf (1923). "Begründung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbarer Veränderlichen mit unendlichem Ausdehnungsbereich" [The foundations of elementary arithmetic established by means of the recursive mode of thought without the use of apparent variables ranging over infinite domains] (PDF). Skrifter Utgit av Videnskapsselskapet I Kristiania. I, Matematisk-naturvidenskabelig Klasse (in German). 6: 1–38.

• JSTOR 2026089
  .

• doi:10.1007/978-94-007-4435-6_8
  .

• Rose, H. E. (1961). "On the consistency and undecidability of recursive arithmetic". Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. 7 (7–10): 124–135.
  MR 0140413
  .