We see here the following statement about Godelization:
Gödel numbering in computer science means more or less "source code" and "data in binary format", so I hope the significance of this should be obvious if I can convince you that this really is so.
Before modern computers came into existence, people made single-purpose computing devices (I am telling you a story, not a history), for example someone made a machine for calculating arctanarctan, and someone else made a machine for calculating the Bessel function. Turing's original insight was that we only had to build one machine (the universal one), which took as input the description of any machine and simulated it. But what is a "description of a machine"? An engineer might think of circuit designs and assembly instructions. But that is very complicated and not easily presented to a machine. And perhaps ever more complicated machines require ever more complicated descriptions?
We need a way of describing machines that is as simple as possible. Here Gödel's idea was important: he showed some years before Turing that all sorts of things in logic (formulas, proofs) could be encoded with numbers, and then manipulated within arithmetic. We can do a similar trick with Turing machines: encode the program, the current state, and the contents of the tape used so far, with a string of symbols on a tape (for examples 00's and 11's), and then manipulate the string with a Turing machine.
In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The data and operators form a mathematical structure which is embedded in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded data in the lambda calculus this way.
Terms that are usually considered primitive in other notations (such as integers, booleans, pairs, lists, and tagged unions) are mapped to higher-order functions under Church encoding. The Church-Turing thesis asserts that any computable operator (and its operands) can be represented under Church encoding. In the untyped lambda calculus the only primitive data type is the function.
This statement appears to combine to two in a way that says they're orthogonal (ie that being church-encoded or not is irrelevant to the Gödelization process) - but I'm not sure:
So let's say that you have natural numbers (or a Church encoding of natural numbers) in your typed lambda calculus. It's possible to do a Gödel numbering that assigns every term in System F to a unique natural number.
My question is: Can we say that Church encoding is a form of Gödelization?