Gödel's method starting with encoding parentheses, and bound variables, i.e. purely syntactical artifacts. It's a good example where you could do away with thi

Gödel's method starting with encoding parentheses, and bound variables, i.e. purely syntactical artifacts. It's a good example where you could do away with this, using e.g. de Bruijn indices -- exactly as you'd suggest switching encoding to binary. It is another layer of (mostly incidental) complexity yet in the end this complexity has to be addressed -- one choice of base does not change the number. When you write programs, you don't prove them correct, and you go down to assembly instructions, which is essentially what Gödel did.