Primitive recursive arithmetic (PRA) is a quantifier-free formalization of the natural numbers.
It was first proposed by Norwegian mathematician Skolem (1923),[1] as a formalization of his finitistic conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitistic.
Many also believe that all of finitism is captured by PRA,[2] but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to ε0,[3] which is the proof-theoretic ordinal of Peano arithmetic.
The language of PRA can express arithmetic propositions involving natural numbers and any primitive recursive function, including the operations of addition, multiplication, and exponentiation.
PRA cannot explicitly quantify over the domain of natural numbers.
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: Especially: PRA replaces the axiom schema of induction for first-order arithmetic with the rule of (quantifier-free) induction: In first-order arithmetic, the only primitive recursive functions that need to be explicitly axiomatized are addition and multiplication.
Defining primitive recursive functions in this manner is not possible in PRA, because it lacks quantifiers.
In this setting a term is a primitive recursive function of zero or more variables.
The rule of induction in Curry's system was unusual.
The rule of induction in Goodstein's system is: 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.
Finally, there are symbols for any primitive recursive functions with corresponding defining equations, as in Skolem's system above.
Logical operators can be expressed entirely arithmetically, for instance, the absolute value of the difference of two numbers can be defined by primitive recursion: Thus, the equations x=y and
express the logical conjunction and disjunction, respectively, of the equations x=y and u=v.