Primitive recursive arithmetic: Difference between revisions

Revision as of 13:35, 15 February 2011

Revision as of 09:39, 18 October 2011

Line 24:

* ... and so on.

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

* From <math>\phivarphi(0)</math> and <math>\phivarphi(x)</math> <math>\to</math> <math>\phivarphi(S(x))</math>, deduce <math>\phivarphi(y)</math>, for any predicate <math>\phivarphi.</math>

In [[first-order arithmetic]], the only [[primitive recursive function]]s 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 function]]s in this manner is not possible in PRA, because it lacks [[quantifier]]s.