I just got back from a week visiting the Canada/USA Mathcamp, where I spent a few days teaching a class on Gödel’s theorems. I only got to the incompleteness theorems on the last day, when I introduced Gödel numbering, showed that some syntactic relations were definable, suggested that provability was therefore definable, and showed that truth (in the standard interpretation) is not definable. Thus, I didn’t get to anything like the full incompleteness theorems, but just showed that there is no recursive set of axioms such that truth in the standard interpretation corresponds to provability from those axioms.
The thing about showing that truth is not definable is that you normally go through satisfaction instead. Given the fact that syntactic relations are definable, we can define functions (which returns the code number for the numeral expressing ) and (which takes as the code of a formula with one free variable, and substitutes in the term that is the code of, and returns the code of the resulting sentence). Then (which says that is the code of a formula satisfied by number ) can be defined in terms of by .
Then, it’s fairly straightforward to show that is not definable. If it were, then we could define , which would have some code number . But then would be true iff didn’t satisfy , which is a contradiction. Therefore, is not definable.
Afterwards, someone pointed out that this proof of the undefinability of doesn’t make any assumption about how the coding works, which seems somewhat surprising. After all, I could take highly non-effective codings, and the undefinability of would still hold. This is surprising, because can be defined under certain encodings. One such encoding is just to separate the sentences into true and false ones, and code them respectively by even and odd numbers, using some sort of lexicographic ordering. Then, since being even and being odd are both definable, truth would be definable as well. But it turns out that no trick like this is going to let satisfaction be definable, because of the diagonalization argument I gave above.
My guess for why this is is because satisfaction requires something like a coding of some of the syntactic structure as well as some of the semantic structure. Standard codings make the syntax definable, but then the semantics fails. Certain bizarre codings let the semantics be definable, but they make the syntax fail. But since the syntax and semantics aren’t recursive in terms of each other, there’s no way to make them both recursive, the way satisfaction seems to require. (Of course, you could probably choose some awful coding that makes both sets of relations undefinable, but why would you want to do that?)
Anyway, going back to camp is always great for precisely this sort of reason – I get to try to teach something new and interesting that I haven’t taught before, and people ask questions that also help me understand the material in a new way.