Primitive recursive arithmetic

From Wikipedia, the free encyclopedia

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

Contents 1 Discussion 2 Language and axioms 3 See also 4 Notes 5 References

[edit] Discussion

Skolem (1923) first proposed PRA as a formalization of his finitist conception of the foundations of arithmetic. Tait^[1] concurs, but Kreisel^[2] deemed finitary systems as strong as Peano Arithmetic. The language of PRA can express arithmetic propositions involving natural numbers and countably infinitely many primitive recursive functions, including the operations of addition, multiplication, and exponentiation. PRA cannot explicitly quantify over the domain of natural 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.

[edit] 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 variable substitution.
The non-logical axioms are:

• ;
• 

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

• 
• 
• 
• 
• ... and so on.

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. All other primitive recursive predicates can be defined using these two primitive recursive functions and quantification over all natural numbers. Defining primitive recursive functions in this manner is not possible in PRA, because it lacks quantifiers.

[edit] See also

• Heyting arithmetic
• Peano arithmetic
• Second-order arithmetic
• primitive recursive function

[edit] 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.

[edit] References

• Feferman, S (1992) What rests on what? The proof-theoretic analysis of mathematics. Invited lecture, 15^th int'l Wittgenstein symposium.
• Thoralf Skolem (1923) "The foundations of elementary arithmetic" in Jean van Heijenoort, translator and ed. (1967) From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931. Harvard Univ. Press: 302-33.