Welcome to PhilSE!
So the Godel definition splits concatenation using Gl(z) into two cases and applies a bounding condition on it. Let's take your example and work through it a bit. In what follows, I'll use the single quotes 'x' to refer to a symbol in the coding scheme, and the double quotes "x" to refer to a string featuring a symbol at each position within the string.
Firstly, let's assume your symbols should also be primes. Let's call 2 the symbol for '0' and code the '=' symbol as 17.
String composition then codes each position in the string as a prime digit, and codes the overall string by raising the prime digits to the prime factors for the symbols. So when thinking about the above as strings of length 1, rather than just as symbols, "0" is coded as 2^2 (symbol 2 in the first position), and "=" is coded as 2^17 (symbol 17 in the first position).
To concatenate these two strings together as "=0" would be to give us the outcome 2^17 * 3^2 - we have taken the '0' symbol from the string "0" and shifted the power of its position one prime factor along.
You might also imagine a godel string with blanks in the other positions, if you allow that the coding for the empty symbol is the number 0. For instance, " 0 " is a string of length 3, but would get the godel code 3^2 (= 2^0 * 3^2 * 5^0)
Now firstly, Godel's numbering definition applies a (fairly liberal) upper bound on the value of its codes. We say "how long are each of our two strings?" If we want to concatenate a string of length 3 and a string of length 2, we'll need to use the first 5 prime numbers to code our outcome. This upper bound should be high enough to outstrip all of the possible values that the lower strings might take, so Godel's approach is to take the highest prime number to an enormous power proportional to the two arguments.
- There's a number theory exercise here to show that 3^(2^17 + 2^2) > 2^17 * 3^2
- Think about it as (3^(2^17)) * (3^(2^2)) > 2^17 * 3^2
- The generalised form of this should intuitively seem true, but I'll leave it as an exercise for you. (This kind of thing is actually great for combinatorial proof methods)
Next, we refine this definition down, and this is where the n Gl x operator comes into effect. When Godel is referring to this operator, this isn't "n times the godel number for formula x" but rather "the code for the string corresponding to the nth symbol of x being in its nth position and all other symbols being null".
So, for example, 1 Gl "=0" would be 2^17, and 2 Gl "=0" would be 3^2.
Hopefully now the definition makes a bit more sense. It's saying "the first l(x) digits of the godel code given by z match the godel code for x, and the subsequent l(y) digits match the godel code for y". "0=0" could (in our model) be coded as (2^2)(3^17)(5^2), and if you've gotten here by concatenating [2^2] & [2^17 * 3^2], the idea is that you've shifted the prime factors of the second half of that concatenation along by the length of the first half.
How do we know this operation has a valid unique solution? Well, one simple (and slightly lazy) argument is that this is simply the Axiom of Choice at work - by defining an upper bound on our definition, if each operation is well enumerated then we're grand. When you see an Epsilon in a definition like you do in the above, it's usually a good bet that Choice is being invoked somewhere. In this case, it's being invoked absolutely unproblematically, because an upper integer bound is being applied in a principled way (as discussed below), but one might potentially be content to just stop here.
But another approach is to look at what we're actually doing by multiplying these prime factors together. Remember, each of our unique symbols is itself a prime number. So what happens when you try to raise a position to something that isn't a prime number? Well, it's just the same thing as creating a new, makeshift symbol that stands in for the whole complex formula, sitting in that position. For example, 5^(x+y) = 5^x * 5^y might be decoded as a string, and x and y are themselves products of prime factors less than 5 - we know there's a solution bigger than our bound that treats this sum as its own symbol value, which we exclude using the first bounding condition - but if we were to think of our particular example of ["0"] & ["=0"] and consider a reduced upper bound for this as 2^x * 5^y (x at position 1, y at position 3), you can see how the work of the coding might start to get a little more clever.
If x is the left value (as given by the second condition), then we only really need to work out the solutions yielded by the third condition, mapping the prime factors of the coding of y to their new values in z. The heavy lifting is being done by Prime Factorization here, and this is the Fundamental Theorem of Arithmetic. In our example of "=0", the key thing is you can determine the proper factorization of the string given by y as (2^17)*(3^2), and this in turn lets you extract what the new godel code for "0=0" should be by shifting the primes along.
Why might this not have seemed so obvious? Well, a lot of people forget the idea that the symbols are also supposed to be primes. This is perhaps the functional difference between symbols and strings - a base symbol is a prime number, and a string can be factorised. But a lot of the surface discussion of Godel coding forgets that step, or thinks it's not important, when in fact it's a very subtle but functionally powerful element of the whole process - it allows for recursive applications of the FTA to allow for more fine-grained extraction of information from strings and string operations at different levels of encoding.
