Primitive recursive arithmetic

From Wikipedia, the free encyclopedia

Primitive recursive arithmetic, or PRA, is a formal system of quantifier-free, or zeroth-order arithmetic, and is considered to be the basic arithmetic of finitism. Its language can express propositions about arithmetic equations involving natural numbers and the operations of addition, multiplication, exponentiation, or any other primitive recursive functions, but it can not express explicit quantification over all numbers. It is often taken as the basic metamathematical formal system for proof theory and especially for consistency proofs such as Gentzen's consistency proof of first-order arithmetic.

[edit] Language and axioms

The language of PRA contains the propositional connectives, the equality symbol =, and a countably infinite number of variables x, y, z, ... which range over the natural numbers. It also contains the constant symbol 0, the successor symbol S (meaning add one), and a symbol for every primitive recursive function, which are also countably infinite in number.

The logical axioms of PRA are the tautologies of propositional calculus and of equality, and it has the logical rules of modus ponens and of substitution of variables. It has the non-logical axioms:

$S(x) \ne 0$
$S(x)=S(y) \to x=y$

As well, it includes, as axioms, recursive defining equations for every primitive recursive function, for instance:

$x+0 = x\$
$x+S(y) = S(x+y)\$
$x.0 = 0\$
$x.S(y) = x.y + x\$
... and so on.

Finally, instead of the axiom of induction for first-order arithmetic, PRA has the rule of (quantifier-free) induction:

$\mbox{From }\phi(0)\mbox{ and }\phi(x) \to \phi(S(x))\mbox{, deduce }\phi(x)\mbox{, for any predicate }\phi.$

In first-order arithmetic, it is unnecessary to include all primitive recursive functions and their defining axioms explicitly. Any primitive recursive predicate can be expressed using only addition, multiplication, and quantification over all natural numbers. However, these cannot be omitted in PRA, as that sort of quantification is not available.