Content deleted Content added
m Deserves its own article, eventually |
First pass; definition. No history, and minimal discussion |
||
Line 1:
'''Primitive recursive arithmetic''', or '''PRA''', is a formal system of [[quantifier]]-free, or [[zeroth order logic|zeroth-order]] arithmetic, and is considered to be the basic arithmetic of [[finitism]]. 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 ==
The language of PRA contains the [[propositional calculus|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 rule of [[modus ponens]]. It has the non-logical axioms:
* <math>S(x) \ne 0</math>
* <math>S(x)=S(y) \to x=y</math>
As well, it includes, as axioms, recursive defining equations for every primitive recursive function, for instance:
* <math>x+0 = x\ </math>
* <math>x+S(y) = S(x+y)\ </math>
* <math>x.0 = 0\ </math>
* <math>x.S(y) = x.y + y\ </math>
* ... and so on.
Finally, instead of the axiom of induction for first-order arithmetic, PRA has the rule of (quantifier-free) induction:
* <math>\mbox{From }\phi(0)\mbox{ and }\phi(x) \to \phi(S(x))\mbox{, deduce }\phi(x)\mbox{, for any predicate }\phi.</math>
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, there cannot be omitted in PRA, as that sort of quantification is not available.
== See also ==
* [[Heyting arithmetic]]
* [[Peano arithmetic]]
* [[Second-order arithmetic]]
== 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.
| |||