Decoding Gödel Numbers for Sequences: A Constructive Approach

[nomadreid]

First, this is not the same question as
https://www.physicsforums.com/threads/goedel-numbering-decoding.484898/
It concerns a different encoding procedure, hence a different decoding one.

My question concerns the argument in http://en.wikipedia.org/wiki/Gödel_numbering_for_sequences
for the existence of an effective decoding function β corresponding to the effective coding π for the Gödel number for sequences as given in that article : that is, given this procedure for generating the Gödel number from a sequence, and given the Godel number G of an unknown sequence (k₁,...k_n), to prove the existence of β such that for all for all 0<i<n, β(G,i) =k_i.

Wikipedia leaves the " for all 0<i<n " implicit, so I will follow that abuse of notation as well:

If I understand that argument correctly:
First, we assume that we can choose m_isuch that
[*] m_i>a_i
[**] all m_i are coprime to one another.
(This can even be done constructively.)

Then since we know that (k₁,...k_n) exists, we know that a least solution x to the congruences
x ≡ a_i mod m_i
exists. Call it X.
We can construct a recursive function rem(a,b) so that rem(a,b)=(a mod b), so since we know X exists, we know that a procedure rem(X,m_i) = a_i exists.

OK, something rankles. Apparently I am not laying down the outline correctly , because it sounds slightly circular to me. Can anyone tell me what is wrong in my summary?

(It would be nice if there were a constructive proof...)

(Also: the construction of the m_iso as to fulfill [*] and [**] would seem to require rather huge numbers: if [*] is fulfilled, then one just takes m = lcm(1,..., n-1) and m_i= (i+1)*m + 1. But the only way I can see to make sure that [*] is fulfilled is to set m = lcm(1,...n-1, G), where G is the given Gödel number of the sequence; this ends up with rather large m_i, so would it still be effective?)

 

[Mark44]

I moved this thread from the Computer Science/Programming section to here. I think this forum section is a better fit.

 

[nomadreid]

Thanks for the actions, Greg Bernhardt and Mark 44. Let me state the question a bit better, including correcting a couple of mistakes in my original post.
In showing the existence of an effective Gödel numbering for sequences, Wikipedia:
in one direction: it takes a known sequence (a₁,...a_n) and establishes a coding procedure which ends up with the Gödel number a ( no problem so far).

Then, to show that a decoding procedure β exists so that β(a,i) = a_i : here's where it gets a bit confusing.
[1] First it finds m such that m is divisible by all the non-zero indices, and then:
[2] constructs a sequence of pairwise coprime numbers m_i
[3] using the CRT (Chinese Remainder Theorem] it shows that, using a pairing function π, that π(x₀,m) = a, whereby x₀ satisfies the system of equations x₀ ≡ a_imod m_i, so that rem(x₀,m_i) = a_i.
By now I am totally lost. Therefore I presume that I have laid out the general argument incorrectly. Could someone either correct this or direct me to a website which lays out the argument a bit more clearly than Wikipedia does? (Yes, I know I can "just" google it, but I didn't come up with anything.)