Primitive recursive arithmetic

Primitive recursive arithmetic, or PRA, is a formalization of arithmetic that is zeroth-order or quantifier-free.

Discussion

Some consider PRA as a formalization of finitism methods in arithmetic ^[1], whereas others deem finitary systems as strong as Peano Arithmetic.^[2]. The language of PRA can express propositions about arithmetic equations involving natural numbers and countably infinitely many primitive recursive functions, including the operations of addition, multiplication, and exponentiation. PRA cannot express explicit quantification over all numbers. PRA is often taken as the basic metamathematical formal system for proof theory, in particular for consistency proofs such as Gentzen's consistency proof of first-order arithmetic.

Language and axioms

The language of PRA consists of:

• A countably infinite number of variables x, y, z,... each ranging over the natural numbers.
• 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 Substitution of variables.
The non-logical axioms are:

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

and recursive defining equations for every primitive recursive function desired, especially:

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

PRA replaces the axiom of schema of induction for first-order arithmetic with the rule of (quantifier-free) induction:

• ${\displaystyle {\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. Defining the primitive recursive functions in this manner is not possible in PRA, because it lacks the universal quantifier.

See also

• Heyting arithmetic
• Peano arithmetic
• Second-order arithmetic

Notes

1. Tait, W.W. (1981) J. of Philosophy 78: 524-46.
2. Georg Kreisel (1958) "Ordinal Logics and the Characterization of Informal Notions of Proof," Proc. Internat. Cong. Mathematicians: 289-99.

References

• Feferman, S. What rests on what? The proof-theoretic analysis of mathematics. Invited lecture, 15^th int'l Wittgenstein symposium, 1992.