A "Gödel numbering for sequences" provides us an effective way to represent each finite sequence of natural numbers as a single natural number. Of course, the embedding is surely possible set theoretically, but the emphasis is on the effectiveness of the functions manipulating such representations of sequences: the operations on sequences (accessing individual members, concatenation) can be "implemented" with using total recursive functions.
It is usually used to build sequential “data types” in the realm of arithmetic-based formalizations of some fundamental notions of mathematics. It is a specific case of the more general idea of Gödel numbering.
E.g. recursive function theory can be regarded as a formalization of notion “algorithm”, and if we regard it as a programming language, we can mimic arrays, lists by encoding a sequence of natural numbers in a single natural number — to achieve this, we can use various number theoretic ideas. Using the fundamental theorem of arithmetic is a straightforward way, but there are also more ergonomic approaches, e.g. using pairing function combined with Chinese remainder theorem in a sophisticated way.[Monk 1976: 56–58] ][Csirmaz 1994: 99–100 (see [http://www.renyi.hu/~csirmaz/l10.ps.gz online] )] ] Gödel numbering
It is a sweeping idea, it can be used to not only sequences, but also whole “architectures” of sophisticated “machines”. We can encode e.g. Markov algorithms,[Monk 1976: 72–74] and also Turing machines][Monk 1976: 52–55] in the realm of natural numbers, this can be used e.g. to prove that the expressing power of recursive function theory is no less than that of the former machine-like formalizations of algorithm.] Accessing members
We expect from any such representation of sequences that we can get back all the information from it that is contained by the original sequence: most important, to access each individual member. We are not sticked necessarily to require that also the length can be obtained directly: even if we want to handle sequences of different length, we can store length data as a surplus member,[ or as the other member of an ordered pair with using a pairing function.]Anyway, we expect that this obtaining back information can be done in an effective way, by an appropriate total recursive function.
We want a totally recursive function "f" that satisfies:For all "n" and for any "n"-length sequence of natural numbers , there exists an appropriate natural number "a", called the Gödel number of the sequence such that for all "i" in the range of 0 … n-1:
There exist effective functions enabling us to obtain back each member of the original sequence from a Gödel number of the sequence. Moreover, there are ways to define some in a constructive way, thus we are not forced to be satisfied with mere proofs of existence.
Gödel's β-function lemma
By an ingenious use of Chinese remainder theorem, we can define constructively such a recursive function (using simple number-theoretical functions, all of which can be defined in a total recursive way) fulfilling the "specifications" given above. Also Gödel defined the function with using Chinese remainder theorem in his article written in 1931. This is a primitive recursive function. [Smullyan 2003: 56 (= Chpt IV, § 5, note 1)]
Thus, for all "n" and for any "n"-length sequence of natural numbers , there exists an appropriate natural number "a", called the Gödel number of the sequence such that[Monk 1976: 58 (= Thm 3.46)] :] Using a pairing function
Our specific solution will depend on a pairing function — there are several ways to implement the latter, let us select one. Now, we can abstract from the details of the “implementation” of the pairing function, we need only to know its “interface”: let , "K", "L" denote the pairing function and its two projection functions, respectively, satisying specification::we shall not discuss and formalize the axiom for excluding alien objects here, it is now not so important.
Using the Chinese remainder theorem
Implementation of the β function
Using the Chinese remainder theorem, we can prove that implementing as:will work, according to the specification we expect to satisfy. We can use a more concise form by an abuse of notation (sort of pattern matching)::Let us achieve even more readability by more modularity and reuse (as these notions are used in computer science[Hughes 1989 (see [http://www.math.chalmers.se/~rjmh/Papers/whyfp.html online] )] ): defining ]