Content deleted Content added
Tag: Reverted |
|||
Line 241:
== 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.
Line 258 ⟶ 259:
== Elimination of parameters ==
{{expert needed|computer science|section|reason=properly explain the purpose of removing parameters (the text only explains *how* it is used, not *what for* - I guess in some Gödelian (un)computability proof)|date=November 2021}}
The primitive recursion schema as given may be replaced by one which makes use of fewer parameters. Let <math>w</math> be an elementary pairing function, and <math>\pi_1,\pi_2</math> be its projection functions for inversion.
| |||