Primitive recursive arithmetic: Difference between revisions

Revision as of 16:58, 14 February 2024

Revision as of 15:56, 20 February 2024

Line 31:

* ... 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>\varphi(0)</math> and <math>\varphi(x)\to\varphi(S(x))</math>, deduce <math>\varphi(y)</math>, for any predicatequantifier-free <math>\varphi.</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 (logic)|quantification]] over all [[natural numbers]]. Defining [[primitive recursive function]]s in this manner is not possible in PRA, because it lacks quantifiers.