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, in showing that the class of arithmetically definable functions is closed under primitive recursion, and therefore includes all primitive recursive functions.

The β function has been 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. Gödel gave the β function its name in (Gödel 1934).

Definition

The function takes three natural numbers as arguments. It is defined as

where denotes the remainder after integer division of by (Mendelson 1997:186).

Properties

The β function is arithmetically definable in an obvious way, because it uses only arithmetic operations and the remainder function which is arithmetically definable. It is therefore representable in Robinson arithmetic and stronger theories such as Peano arithmetic. 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.

Concretely, if f is a function defined by primitive recursion on a parameter 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. While that is not possible directly, one can say instead: there exist natural numbers a and b such that β(a,b,0) = c, β(a,b,n) = y and for all i < n one has g(i, β(a,b,i)) = β(a,b,i+1).

The β function lemma

The utility of the β function comes from the following result, which is the purpose of the β function in Gödel's incompleteness proof (Gödel 1931). This result is explained in more detail than in Gödel's proof in (Mendelson 1997:186) and (Smith 2013:113-118).

β function lemma. For any sequence of natural numbers (k0, k1, …, kn), there are natural numbers b and c such that, for every i ≤ n, β(b, c, i) = ki.

The proof of the β function lemma makes use of the Chinese remainder theorem.

gollark: Just use the service, utter.
gollark: This is just Macron but in hardware.
gollark: This is helpful, right?
gollark: https://lichess.org/xzvtDrGM
gollark: I am INCREDIBLY competent.

See also

References
  • Martin Davis, ed. (1965). The Undecidable – Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions. Dover Publications. ISBN 9-780-48643-2281.
  • Kurt Gödel (1931). "Über formal unentscheidbare Sätze der "Principia Mathematica" und verwandter Systeme I". Monatshefte für Mathematik und Physik (in German). 28. pp. 173–198. in (Gödel 1986)
  • Kurt Gödel (1934). "On undecidable propositions of formal mathematical systems". Notes taken by Stpehen C. Kleene and John B. Rosser during lectures given at the Institute for Advanced Study. Reprinted in (Davis 1965)
  • Kurt Gödel (1986). Solomon Feferman; John W. Dawson Jr; Stephen C. Kleene; Gregory H. Moore; Robert M. Solovay; Jean van Heijenoort (eds.). Kurt Gödel – Collected Works (in German and English). I – Publications 1929-1936. Oxford University Press. ISBN 0-195-14720-0.
  • Elliott Mendelson (1997). Introduction to Mathematical Logic (4th ed.). CRC Press. ISBN 0-412-80830-7.
  • Wolfgang Rautenberg (2010). A Concise Introduction to Mathematical Logic (3rd ed.). New York: Springer Science+Business Media. p. 244. doi:10.1007/978-1-4419-1221-3. ISBN 978-1-4419-1220-6.
  • Peter Smith (2013). An Introduction to Gödel's Theorems (2nd ed.). UK: Cambridge University Press. ISBN 978-1-107-02284-3.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.