|
* #G: If φ satisfies the equation:
:: φ(y,'''x''') = χ(y, COURSE-φ(y; x<sub>2</sub>, ... x<sub>n</sub> ), x<sub>2</sub>, ... x<sub>n</sub> then φ is primitive recursive in χ. The value COURSE-φ(y; '''x'''<sub>2 to n</sub> ) of the course-of-values function encodes the sequence of values φ(0,'''x'''<sub>2 to n</sub>), ..., φ(y-1,'''x'''<sub>2 to n</sub>) of the original function.
== Use in first-order Peano arithmetic ==
{{expert needed|computer science|section|reason=properly explain the purpose of using the β function (the text only explains *how* it is used, not *what for* - I guess in some Gödelian (un)computability proof)|date=November 2021}}
In [[first-order logic|first-order]] [[Peano arithmetic]], there are infinitely many variables (0-ary symbols) but no [[arity|k-ary]] non-logical symbols with k>0 other than S, +, *, and ≤. Thus in order to define primitive recursive functions one has to use the following trick by Gödel.
By using a [[Gödel numbering for sequences]], for example [[Gödel's β function]], any finite sequence of numbers can be encoded by a single number. Such a number can therefore represent the primitive recursive function until a given n.
Let ''h'' be a 1-ary primitive recursion function defined by:
:<math> h(0) = C</math>
:<math> h(n+1) = g(n,h(n))</math>
where C is a constant and ''g'' is an already defined function.
Using Gödel's β function, for any sequence of natural numbers (k<sub>0</sub>, k<sub>1</sub>, ..., k<sub>n</sub>), there are natural numbers b and c such that, for every i ≤ n, β(b, c, i) = k<sub>i</sub>. We may thus use the following formula to define ''h''; more precisely, ''m''=''h''(''n'') is a shorthand for the following:
:<math>\exists b: \exists c: \beta(b, c, 0) = C \land \forall i: (i<n) \rightarrow (\beta(b, c, i+1) = g(i,\beta(b, c, i))) \land (m = \beta(b, c, n))</math>
and the equating to ''g'', being already defined, is in fact shorthand for some other already defined formula (as is β, whose formula is given [[Gödel's β function|here]]).
The generalization to any k-ary primitive recursion function is trivial.
== Elimination of parameters ==
| 