Gödel's β function

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, as a step in the extension of the language of Peano arithmetic to include all primitive recursive functions.

Definition

The β function takes three natural numbers as arguments. It is defined as follows (Mendelson 1997:186):

β(x₁,x₂,x3) = rem(1+(x₃+1)·x₂, x₁).

Here the remainder function rem(x,y) takes two natural numbers as arguments and returns the natural number remainder when x is divided by y.

Properties

The β function is a primitive recursive function. It is representable in Peano arithmetic.

The β lemma

The utility of the β function comes from the following result (Mendelson 19997:186), which is also due to Gödel.

The β Lemma. For any sequence of natural numbers (k₀,k₁,...,k_n), there are natural numbers b and c such that, for every i≤n, β(b,c,i) = k_i.

References

• Elliott Mendelson (1997), Introduction to Mathematical Logic, 4th edition, CRC press. ISBN 0-412-80830-7

External links

• Stephen Simpson, Foundations of Mathematics lecture notes, section 2.2.