Primitive recursive arithmetic: Difference between revisions

Revision as of 13:31, 2 April 2023

Revision as of 13:36, 2 April 2023

Line 19:

* <math>S(x) \neq 0</math>;

* <math>S(x)=S(y) \to x = y,</math>

so that <math>S(0) = 0</math> is falsenegated and where <math>x \neq y</math> denotes <math>x = y \to \bot</math>.

Further, recursive defining equations for every [[primitive recursive function]] may be adopted as axioms as desired. For instance, the most common characterization of the primitive recursive functions is as the 0 constant and successor function closed under projection, composition and primitive recursion. So for a (''n''+1)-place function ''f'' defined by primitive recursion over a ''n''-place base function ''g'' and (''n''+2)-place iteration function ''h'' there would be the defining equations: