Content deleted Content added
Recursuve -> primitive recursive |
m typo |
||
Line 9:
:If ''f''(''x'',''z''<sub>1</sub>,''z''<sub>2</sub>,...,''z''<sub>''n''</sub>) is a partial function on the [[natural numbers]] with ''n''+1 arguments ''x'', ''z''<sub>1</sub>,...,''z''<sub>''n''</sub>, then the function μ''x'' ''f'' is the partial function with arguments ''z''<sub>1</sub>,...,''z''<sub>''n''</sub> that returns the least ''x'' such that ''f''(0,''z''<sub>1</sub>,''z''<sub>2</sub>,...,''z''<sub>''n''</sub>), ''f''(1,''z''<sub>1</sub>,''z''<sub>2</sub>,...,''z''<sub>''n''</sub>), ..., ''f''(''x'',''z''<sub>1</sub>,''z''<sub>2</sub>,...,''z''<sub>''n''</sub>) are all defined and ''f''(''x'',''z''<sub>1</sub>,''z''<sub>2</sub>,...,''z''<sub>''n''</sub>) = 0, if such an ''x'' exists; if no such ''x'' exists, then μ''x'' ''f'' is not defined for the particular arguments ''z''<sub>1</sub>,...,''z''<sub>''n''</sub>.
It is easy to see that this least search axiom (along with the simple primitive recursion axioms) implies the bounded search axiom of primitive
The set of ''partial recursive functions'' is defined as the smallest set of partial functions of any [[arity]] from natural numbers to natural numbers which contains the zero, successor, and projection functions, and which is closed under composition, primitive recursion, and unbounded search.
| |||