While a set theoretical embedding is surely possible, 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 arithmetic-based formalizations of some fundamental notions of mathematics.
For example, recursive function theory can be regarded as a formalization of the notion of an algorithm, and can be regarded as a programming language to mimic lists by encoding a sequence of natural numbers in a single natural number.
For example, we can encode Markov algorithms,[3] or Turing machines[4] into natural numbers and thereby prove that the expressive 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, each individual member must be retrievable.
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 with the property that for all n and for any n-length sequence of natural numbers
By an ingenious use of the Chinese remainder theorem, we can constructively define 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.
function using the Chinese remainder theorem in his article written in 1931.
We can use a more concise form by an abuse of notation (constituting a sort of pattern matching): Let us achieve even more readability by more modularity and reuse (as these notions are used in computer science[8]): by defining
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.
solution of the simultaneous congruence system also satisfies A stronger assumption for m requiring
The proof is by contradiction; assume the 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,
, thus (as equality axioms postulate identity to be a congruence relation[10]) we get Since p is a prime element (note that the irreducible element property is used), we get Now we must resort to our assumption The assumption was chosen carefully to be as weak as possible, but strong enough to enable us to use it now.
Thus (as equality axioms postulate identity to be a congruence relation [10]) can be proven.
However, in the negation of the original statement p is existentially quantified and restricted to primes
By reaching contradiction with its negation, we have just proven the original statement: We build a system of simultaneous congruences We can write it in a more concise way: Many statements will be said below, all beginning with "
are pairwise comprime as proven in the previous sections, so we can refer to the solution ensured by the Chinese remainder theorem.
as satisfying which means (by definition of modular arithmetic) that Recall the second assumption, “
implies 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
Although proving this was most important for establishing an encoding scheme for sequences, we have to fill in some gaps yet.
Our ultimate question is: what number should stand for the encoding of sequence
We want a constructive and algorithmic connection: a (total) recursive function that performs the encoding.
This gap can be filled 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
In fact, the specification plays a role here of a more general notion (“special function”[12]).
function:[5] It can be proven (using the notions of the previous section ) that g is (total) recursive.
In other words, we may encode sequences in an analogous way to lists in programming.
To illustrate both cases: if we form the Gödel numbering of a Turing machine, then the each row in the 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.
[14] But if we want to reason about configuration-like things (of Turing-machines), and specifically if 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.