'''Primitive recursive arithmetic''', or '''PRA''', is a formal system of [[quantifier]]-free, or [[zeroth order logic|zeroth-order]] arithmetic. On some views, andit is considered to be the basicformalization of [[finitary|finitism]] methods in arithmetic <ref>Tait, W.W., J. of Philosophy 78, 524-46 (1981)</ref>, whereas on others systems as strong as [[finitismPeano Arithmetic]] may be seen as finitary <ref>Kreisel, G., Ordinal Logics and the Characterization of Informal Notions of Proof, Proc. Internat. Cong. Mathematicians 289-99 (1958)</ref>. Its language can express propositions about arithmetic equations involving [[natural number]]s and the operations of addition, multiplication, exponentiation, or any other [[primitive recursive function]]s, but it can not express explicit quantification over all numbers. It is often taken as the basic [[metamathematic]]al formal system for [[proof theory]] and especially for [[consistency proof]]s such as [[Gentzen's consistency proof]] of [[first-order arithmetic]].
== Language and axioms ==
Line 25:
== References ==
* [[Solomon Feferman|Feferman, S]]. ''[http://citeseer.ist.psu.edu/feferman92what.html What rests on what? The proof-theoretic analysis of mathematics]''. Invited lecture, 15<sup>th</sup> int'l Wittgenstein symposium, 1992.
