Primitive recursive arithmetic: Difference between revisions

Revision as of 16:54, 18 December 2010

Revision as of 13:35, 15 February 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>\phi(0)</math> and <math>\phi(x)</math> <math>\to</math> <math>\phi(S(x))</math>, deduce <math>\phi(xy)</math>, for any predicate <math>\phi.</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.