A similar question is why are some Turing machines universal and some aren't? Or, more generally, why can you prove some Turing machines halt on all inputs and

A similar question is why are some Turing machines universal and some aren't? Or, more generally, why can you prove some Turing machines halt on all inputs and for some you cannot? I think what you mean by "encoding" is what I mean by "being able to write an interpreter." It's not hard to encode mathematical statements as real numbers in the axioms of a real closed field, which someone outside the theory is easily able to decode. However, the fact the theory is complete implies there is no way to write an interpreter within the theory. There are other kinds of interpreters you might be interested in. For example, one that determines absolute truth of a statement, that is, the truth of the statement in the "Platonic universe," whether or not it is provable. You can still apply the usual kind of argument, if such an interpreter existed, to generate a sentence that is true iff it is false. I imagine a heuristic sort of issue is that to write such an interpreter you need to be able to encode environments (like in a Scheme interpreter), but the set of possible environments is too big in a Russell's paradox sort of way. In model theory, they call such a function, when restricted to a particular model, a truth term. > expressive enough to encode itself via Gödel numbering -- and hence construct "the Gödel sentence". Once you have the Gödel sentence, the consequences re: diagonalization [...] are readily understood I don't really understand you here: a diagonalization/Lawvere-like argument is how the Gödel sentence is constructed in the first place.