- Primitive recursive arithmetic
**Primitive recursive arithmetic**, or**PRA**, is aquantifier -free formalization of the natural numbers. It was first proposed by Skolem [] as a formalization of hisThoralf Skolem (1923) "The foundations of elementary arithmetic" inJean van Heijenoort , translator and ed. (1967) "From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931". Harvard Univ. Press: 302-33.finitist conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitist. Many also believe that all of finitism is captured by PRA [*Tait, W.W. (1981) "J. of Philosophy 78": 524-46.*] , but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to ε_{0}[] , which is the proof-theoretic strength ofGeorg Kreisel (1958) "Ordinal Logics and the Characterization of Informal Notions of Proof," "Proc. Internat. Cong. Mathematicians": 289-99.Peano arithmetic . PRA is sometimes called**Skolem arithmetic**.The language of PRA can express arithmetic propositions involving

natural number s and anyprimitive recursive function , including the operations ofaddition ,multiplication , andexponentiation . PRA cannot explicitly quantify over the domain of natural numbers. PRA is often taken as the basicmetamathematic alformal system forproof theory , in particular forconsistency proof s such asGentzen's consistency proof offirst-order arithmetic .**Language and axioms**The language of PRA consists of:

* Acountably infinite number of variables "x", "y", "z",... each ranging over thenatural number s.

*The propositional connectives;

*The equality symbol "=", the constant symbol "0", and the successor symbol "S" (meaning "add one");

*A symbol for eachprimitive recursive function .The logical axioms of PRA are the:

* Tautologies of thepropositional calculus ;

* Usual axiomatization ofequality as anequivalence relation .The logical rules of PRA aremodus ponens and variable substitution.

The non-logical axioms are:

* $S(x)\; e\; 0$;

* $S(x)=S(y)\; o\; x=y,$and recursive defining equations for everyprimitive recursive function desired, especially:

* $x+0\; =\; x$

* $x+S(y)\; =\; S(x+y)$

* $x\; cdot\; 0\; =\; 0$

* $x\; cdot\; S(y)\; =\; xy\; +\; x$

* ... and so on.PRA replaces the axiom schema of induction forfirst-order arithmetic with the rule of (quantifier-free) induction:

* $mbox\{From\; \}phi(0)mbox\{\; and\; \}phi(x)\; o\; phi(S(x))mbox\{,\; deduce\; \}phi(x)mbox\{,\; for\; any\; predicate\; \}phi.$In

first-order arithmetic , the onlyprimitive recursive function s that need to be explicitly axiomatized areaddition andmultiplication . All other primitive recursive predicates can be defined using these two primitive recursive functions andquantification over allnatural numbers . Definingprimitive recursive function s in this manner is not possible in PRA, because it lacksquantifier s.**Logic-free calculus**It is possible to formalise PRA in such a way that it has no logical connectives at all - a sentences of PRA is just an equation between two primitive recursive functions of zero or more variables. In 1941

Haskell Curry gave the first such system [] , which had a non-elementary rule of induction. This was later refined byHaskell Curry , " [*http://www.jstor.org/stable/2371522 A Formalization of Recursive Arithmetic*] ".American Journal of Mathematics , vol 63 no 2 (1941) pp 263-282Reuben Goodstein [] . The rule of induction in the latter system is:Reuben Goodstein , " [*http://www.digizeitschriften.de/resolveppn/GDZPPN002343355 Logic-free formalisations of recursive arithmetic*] ",Mathematica Scandinavica vol 2 (1954) pp 247-261$\{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 funcions which may have parameters other than the ones shown. The rules of substitution in this system are:

$\{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 primitive recursive functions of zero or more variables. Finally, as above, there are the defining equations for any primitive recursive functions needed.

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:

$egin\{align\}\; P(0)\; =\; 0\; quad\; quad\; P(S(x))\; =\; x\; \backslash \; x\; dot\; -\; 0\; =\; x\; quad\; quad\; x\; dot\; -\; S(y)\; =\; P(x\; dot\; -\; y)\; \backslash $

x - y| = & (x dot - y) + (y dot - x) \end{align}Thus, the equations x=y and |"x"-"y"|=0 are equivalent. Therefore the equations $|x\; -\; y|\; +\; |u\; -\; v|\; =\; 0\; !$ and $|x\; -\; y|\; cdot\; |u\; -\; v|\; =\; 0\; !$ express the logical

conjunction anddisjunction , respectively, of the equations "x"="y" and "u"="v".Negation can be expressed as $1\; dot\; -\; |x\; -\; y|\; =\; 0$.**See also***

Heyting arithmetic

*Peano arithmetic

*Second-order arithmetic

*primitive recursive function **External links*** Feferman, S (1992) " [

*http://citeseer.ist.psu.edu/feferman92what.html What rests on what? The proof-theoretic analysis of mathematics*] ". Invited lecture, 15^{th}int'l Wittgenstein symposium.**References**

*Wikimedia Foundation.
2010.*