Gödel numbering for sequences
In mathematics, 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" using total recursive functions, and in fact by primitive 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 economic approaches, e.g. using pairing function combined with Chinese remainder theorem in a sophisticated way.
Besides using Gödel numbering to encode unique sequences of symbols into unique natural numbers (i.e. place numbers into mutually exclusive or one-to-one correspondence with the sequences), we can use it to encode whole “architectures” of sophisticated “machines”. For example we can encode Markov algorithms, or Turing machines into natural numbers and thereby prove that the expressing power of recursive function theory is no less than that of the former machine-like formalizations of algorithms.
Any such representation of sequences should contain all the information as in the original sequence: most importantly, to access each individual member. However, the length does not have to match 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 by using a pairing function.
Anyway, we expect that there is an effective way for this information retrieval process in form of an appropriate total recursive function.
We want to find 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 are effective functions which can retrieve each member of the original sequence from a Gödel number of the sequence. Moreover, we can define some of them in a constructive way, so we can go well beyond 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 using the Chinese remainder theorem in his article written in 1931. This is a primitive recursive function.
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
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.
Remainder for natural numbers
We shall use another auxiliary function: it will compute the remainder for natural numbers. Examples:
It can be proven that this function can be "implemented" as a recursive function.
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): defining the sequence , enables us to write
We shall use this notation also in the proof.
For proving the correctness of the above definition of function, we shall use (and prove) several auxiliary theorems, lemmas. These have their own assumptions. Now we try to find out these assumptions, calibrating and tuning their strength carefully: they should not be said in an either superfluously sharp, or unsatisfactorily weak form.
Let be a sequence of natural numbers. Let m be chosen to satisfy
The first assumption is meant as
It is needed to meet an assumption of the Chinese remainder theorem (that of being pairwise coprime). In the literature, sometimes this requirement is replaced with a stronger one, e.g. constructively built with the factorial function, but the proof uses just as much strength as formulated here.
The second assumption does not concern the Chinese remainder theorem in any way. It will have importance in proving that the specification for is met eventually. It ensures that an solution of the simultaneous congruence system
A stronger assumption for m requiring automatically satisfies it (if we define the notation as above).
Proof that (coprimality) assumption for Chinese remainder theorem is met
We shall prove that the (coprimality) assumption for Chinese remainder theorem is met.
As mentioned in section Hand-tuned assumptions, we prescribed that
thus we can use it.
What we want to prove is that we can produce a sequence of pairwise coprime numbers in a way that will turn out to correspond to the Implementation of the β function in a sense.
Let us use reductio ad absurdum!
Negation of the original statement:
We know what “coprime” relation means (in a lucky way, its negation can be formulated in a concise form), thus, let us substitute in the appropriate way:
Using a “more” prenex normal form (but note allowing a constraint-like notation in quantifiers):
Because of a theorem on divisibility, allows us to say also
Substituting the definens of -sequence notation, we get , thus (as equality axioms postulate identity to be a congruence relation ) we get
Using that p is a prime element (note: not the irreducible element property is used!), we get
Resorting to the first hand-tuned assumption
Now this is the point in the proof where we must resort to our assumption
let us remember, we have planned this assumption calibrated carefully to be as weak as possible, but strong enough to enable us to use it now.
The assumed negation of the original statement (let us remember, we use reductio ad absurdum) contains an appropriate existential statement using indices , this entails , thus the mentioned assumption can be applied, so holds.
Using an (object) theorem of the propositional calculus as a lemma
We can prove by several means  known in propositional calculus, that
Because entails (by the transitivity property of the divisibility relation) that , thus (as equality axioms postulate identity to be a congruence relation )
can be proven.
Reaching the contradiction
The negation of original statement contained
and we have just proved
should hold. But, after substituting the definiens for , we shall see
Thus, summarizing the above three statements, by transitivity of the equality, also
should hold. But let us look up the quantification of p in the negation of the original statement: p is existentially quantified and restricted to primes
The above statement together with the above quantification of p establish the contradiction we wanted to reach.
End of reductio ad absurdum
By reaching contradiction with its negation, we have just proven the original statement:
The system of simultaneous congruences
We build a system of simultaneous congruences
We can write it in a more concise way:
In the followings, many statements will be said, all beginning with . To achieve a more ergonomic treatment, from now on all statements will be regarded in the scope of an quantification. Thus: begins!
Let us chose a solution for the system of simultaneous congruences. At least one solution must exist, because are pairwise comprime (that's what we have been proving so long in the previous sections!), thus we can refer to the Chinese remainder theorem's ensuring solution. Thus, from now on, we can regard satisfying
it means (by definition of modular arithmetic) that
Resorting to the second hand-tuned assumption
Again, we must resort to the assumptions whose strength we specifically “tuned” for using in the proof. But now, it is the second assumption (which does not concern the Chinese remainder theorem in any way) that we need: “”. Let us remember: we are now in the scope of a “big” quantification for i, thus we don't repeat its quantification for each statement.
The second hand-tuned assumption will join in at this point, because it entails that
Now by transitivity of equality we get
Our original goal was to prove that the definition
is good for achieving what we declared in the specification of : we want to hold.
That's it, it can be seen now by transitivity of equality, looking at the above three equations.
Scope of i ends here.
Existence and uniqueness
We have just proven the correctness of the definition of : its specification requiring
is met. Although proving this was the most important, if we want to establish an encoding scheme for sequences, but we have to fill in some gaps yet. These are related notions similar to existence and uniqueness (although on uniqueness, “at most one” should be meant here, and the conjunction of both is delayed as a final result).
Uniqueness of encoding, achieved by minimalization
Because let us remember, our ultimate question is: what number should stand for the encoding of sequence ? The specification declares only an existential quantification, not yet a functional connection. We want a constructive and algorithmic way, even more, a (total) recursive function for the encoding.
Totality, because minimalization is restricted to special functions
This gap can be filled in in a straightforward way: we shall use minimalization, and the totality of the resulting function is ensured by everything we have proven till now (i.e. the correctness of the definition of by meeting its specification). In fact, the specification
plays a role here of a more general notion (“special function”). The importance of this notion is that it enables us to split off the (sub)class of (total) recursive functions from the (super)class of partial recursive functions. In brief, the specification says exactly: a function f  satisfying specification
is a special function, i.e. for each fixed combination of all-but-last arguments, the function f has root in its last argument:
The Gödel numbering function g can be chosen to be total recursive
Thus, let us choose the minimal possible number that fits well in the specification of the function:
and it can be proven (using the notions of the previous section ) that g is (total) recursive.
Access of length
If we use the above scheme for encoding sequences only in contexts where the length of the sequences is fixed, then no problem arises. In other words, we can use them in an analogous way as arrays are used in programming.
But sometimes we need dynamically stretching sequences, or we need to deal with sequences whose length cannot be typed in a static way. In other words, we may encode sequences in an analogous way as we use lists in programming.
An example for both cases: if we make the Gödel numbering of a Turing machine, then the each row in matrix of the “program” can be represented with tuples, sequences of fixed length (thus, without storing the length), because the number of the columns is fixed. But if we want to reason about configuration-like things (of Turing-machines), and specially, we want to encode the significant part of the tape of a running Turing machine, then we have to represent sequences together with their length. Moreover, we can mimic dynamically stretching sequences by representing sequence concatenation (or at least, augmenting a sequence with one more element) with a [totally] recursive function.
Length can be stored simply as a surplus member:
The corresponding modification of the proof is straightforward, by adding a surplus
to the system of simultaneous congruences (provided that the surplus member index is chosen to be 0). Also the assumptions etc. have to be modified accordingly.
- ↑ 1.0 1.1 Monk 1976: 56–58
- ↑ 2.0 2.1 Csirmaz 1994: 99–100 (see online)
- ↑ Monk 1976: 72–74
- ↑ Monk 1976: 52–55
- ↑ 5.0 5.1 5.2 5.3 Csirmaz 1994: 100 (see online)
- ↑ Smullyan 2003: 56 (= Chpt IV, § 5, note 1)
- ↑ Monk 1976: 58 (= Thm 3.46)
- ↑ Hughes 1989 (see online)
- ↑ Burris 1998: Supplementary Text, Arithmetic I, Lemma 4
- ↑ 10.0 10.1 see also related notions, e.g. “equals for equals” (referential transparency), and another related notion Leibniz's law / identity of indiscernibles Cite error: Invalid
<ref>tag; name "congid" defined multiple times with different content
- ↑ either proof theoretic (algebraic steps); or semantic (truth table, method of analytic tableaux, Venn diagram, Veitch diagram / Karnaugh map)
- ↑ Monk 1976: 45 (= Def 3.1.)
- ↑ E.g. defined by
- ↑ Monk 1976: 53 (= Def 3.20, Lem 3.21)
- ↑ Csirmaz 1994: 101 (=Thm 10.7, Conseq 10.8), see online
|CitationClass=book }} Each chapter is downloadable verbatim on author's page.
|CitationClass=journal }} Template:Dead link
|CitationClass=book }} Translation of Smullyan 1992.