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₂, x₃) = rem(x₁, 1 + (x₃ + 1) · x₂).

Where rem(x, y) denotes the remainder after integer division of x by y.

Properties

The β function is a primitive recursive function. It is representable in Robinson arithmetic and stronger theories such as Peano arithmetic.

The β lemma

The utility of the β function comes from the following result (Mendelson 1997: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.

This follows from the Chinese remainder theorem.

See also

• Gödel numbering for sequences
• Gödel's incompleteness theorems
• Diagonal lemma

References

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

External links

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