What are the formal properties of Godel numbering that are required to make it 'work'? Godel numbering assigns a number to every formula. It appears to me that any encoding will do. However its also apparent, though I'm not sure how, that certain properties of the encoding used in Godel numbering are important for the purposes of the proof of the incompleteness theorem. 
What are these properties? Are they to do with effectiveness in some way? 
 A: Take some version of the original Gödel scheme $g\colon E \to \mathbb{N}$ for mapping expressions to numbers, and some alternative scheme $f\colon E \to \mathbb{N}$. Then the natural requirement for $f$ to be an "acceptable" alternative scheme is that there is a pair of primitive recursive "translation" functions $t$, $t'$ for getting from code numbers under one scheme to code numbers under the other. That is to say, we have  $g(e) = t(f(e))$ and $f(e) = t'(g(e))$ for any expression $e$. [We can get from one coding to the other by a computation that doesn't involve open-ended searches.]
If this holds, then all the arithmetization of syntax using a Gödelian scheme $g$ will go over to arithmetization of syntax by alternative scheme $f$ preserving primitive recursiveness. In other words, if  e.g. the property of numbering-a-wff is primitive recursive under one numbering scheme it will be primitive recursive under the other. And then all the usual constructions and proofs can be done with the new scheme (perhaps with greater elegance or more clumsily, depending on details) as were done with the original scheme.
[Fine print. After Gödel's original paper it was quickly realized that it is usually enough for the arithmetized syntactic properties to be recursive under coding (as opposed to primitive recursive), since nearly any theory that can represent all the primitive recursive functions can represent the recursive functions too. So in fact it is usually enough that a new coding scheme is recursively translatable into the original Gödel scheme for everything still to go through. But, as far as I know, any coding scheme for an ordinary kind of theory that you are likely to dream up without positively trying to be perverse will be primitively recursively related to Gödel's original scheme: for why on earth would you build a need for unbounded searches into a coding scheme?] 
