In mathematical logic, Gödel's β function is a function used to permit quantification over finite sequences of natural numbers in formal theories of arithmetic.
The β function is used, in particular, in showing that the class of arithmetically definable functions is closed under primitive recursion, and therefore includes all primitive recursive functions.
The β function was introduced without the name in the proof of the first of Gödel's incompleteness theorems (Gödel 1931).
The β function lemma given below is an essential step of that proof.
function takes three natural numbers as arguments.
denotes the remainder after integer division of
The β function is arithmetically definable in an obvious way, because it uses only arithmetic operations and the remainder function which is arithmetically definable.
By fixing the first two arguments appropriately, one can arrange that the values obtained by varying the final argument from 0 to n run through any specified (n+1)-tuple of natural numbers (the β lemma described in detail below).
This allows simulating the quantification over sequences of natural numbers of arbitrary length, which cannot be done directly in the language of arithmetic, by quantification over just two numbers, to be used as the first two arguments of the β function.
For example, if f is a function defined by primitive recursion on a recursion variable n, say by f(0) = c and f(n+1) = g(n, f(n)), then to express f(n) = y one would like to say: there exists a sequence a0, a1, ..., an such that a0 = c, an = y and for all i < n one has g(i, ai) = ai+1.
The primitive recursion schema as given may be replaced by one which makes use of fewer parameters.
Theorem: Any function constructible via the clauses of primitive recursion using the standard primitive recursion schema is constructible when the schema is replaced with the following.
This is proven by providing two intermediate schemata for primitive recursion, starting with a function defined via the standard schema, and translating the definition into terms of each intermediate schema and finally into terms of the above schema.
The first intermediate schemata is as follows: Translation of the standard definition of a primitive recursive function to the intermediate schema is done inductively, where an elementary pairing function
-ary primitive recursive function, terminating the induction at
Translation to it is accomplished by pairing
from these paired images by taking
Finally, translation of the intermediate schema into the parameter-eliminated schema is done with a similar pairing and unpairing of
Composing these three translations gives a definition in the original parameter-free schema.
[1] This allows primitive recursion to be formalized in Peano arithmetic, due to its lack of extra n-ary function symbols.
[citation needed] The utility of the β function comes from the following result (Gödel 1931, Hilfssatz 1, p. 192-193), which is the purpose of the β function in Gödel's incompleteness proof.
This result is explained in more detail than in Gödel's proof in (Mendelson 1997:186) and (Smith 2013:113-118).
As an example, the sequence (2,0,2,1) can be encoded by b=3412752 and c=24, since The proof of the β function lemma makes use of the Chinese remainder theorem.