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.

Sridhar(22:12:19) :I believe there’s a typo at the end of your second paragraph; the final instance of “NUMERAL(Z)” should be “NUMERAL(Y)” instead. [Ed: fixed now]

Sridhar(23:05:02) :I like to view the phenomenon of indefinability of satisfaction as essentially just a reshaping of Cantor’s Theorem. Normally, one takes Cantor’s Theorem merely to say “For every function f from X to (unary) predicates on X, there is some predicate on X which is not in f’s range”. But, of course, when one looks at the diagonalization proof and considers the relative definability of the diagonal, one sees that the conclusion can (and, I say, should) be worded in a stronger fashion, as the statement “For every function f from X to predicates on X, there is some predicate on X which is definable from f but not in f’s range”. If we then take the tiny additional step of limiting our consideration to the case where f is itself definable, we get that there is some definable predicate on X which is not in f’s range; i.e., we obtain that there is no definable surjection from X to the definable predicates on X. As the notion of “a surjection from X to its definable predicates” is just the same as the notion of “a curried version of the satisfaction relation on X under some encoding (of definable predicates on X as members of X)”, this means we have obtained precisely the indefinability of satisfaction in a very general and elegant way.

Of course, this is exactly the same, except for perhaps the perspective of the approach, as the argument above, but it is the perspective which impresses me; that the indefinability of satisfaction is pretty much the same fact, in some sense, as Cantor’s Theorem, despite the latter being presumably so much better known than the former.

I then think of the indefinability of truth under standard encodings of sentences as then something of a technical curiosity which happens to arise as a consequence of this more fundamental discovery (of Cantor’s Theorem in its full strength). This would be similar to, say, knowledge of the fact that the decision problem for first-order logic is undecidable in the presence of a single binary relation or of two unary functions or whatever the various minimality results are, I don’t even know; it’s an interesting, in a way, that the machinery needed for the fundamental result can be reduced, through various tricks, to such things, but the real crux of the phenomenon, the location of all the important action and where to go to find insight, would be in the pre-reduced version. (The incompleteness of PA is a similar thing; it’s interesting that the machinery for encoding sequences, and through them computable functions, can be reduced to natural number addition and multiplication, but this is also basically a parlor trick)

Of course, since discussions of TRUTH are discussions of a big, important, capital-letter word in a way which discussions of satisfaction or surjections into power sets are not, it’s to be expected that people will naturally get caught up in viewing the phenomenon from that end. But if one really wants to wrap one’s mind around it, I think thinking about the phenomenon as fundamentally a phenomenon about truth is misguided.

Kenny(09:22:38) :I would agree that the actual coding of everything relevant in terms of addition and multiplication is basically a parlor trick. However, the fact that bounded quantifier arithmetic is in some important sense equivalent to Turing machines is fairly deep, I would think. Arithmetic isn’t just some branch of mathematics that we thought of at some point – it really is one of the most basic in a very natural sense. The fact that it’s also equivalent to the most general idea of computation is interesting, especially given that real number arithmetic isn’t.

Anyway, that’s quite interesting to see that something like Cantor’s Theorem is the basic result here. Although, if you’re talking about a surjection onto

definablepredicates, then there’s something like a truth or satisfaction notion right there in the notion of definability. So it’s not totally clear to me which one I would put as more basic. Cantor’s Theorem was understood decades before Gödel’s theorems, but it’s also true that the liar paradox was known millenia before that.Sridhar(14:03:46) :Yeah, the notion of definability does perhaps contain within itself notions like truth or satisfaction. Interestingly, in Cantor’s proof, the diagonal isn’t merely first-order definable from f, it’s actually quantifier-freely definable from f, so we needn’t even talk about first-order definability, merely quantifier-free definability.

Actually, I view the fundamental result in Cantor’s proof as something even more general, a sort of fixed-point result: Given f : A -> (A ->B) and g : B -> B, there is some D : A -> B such that D is very simply definable from f and g, and satisfies the property that the image under D of the preimage under f of D contains only fixed points of g. Furthermore, this can be done uniformly, in the sense that there is a fixed definition of D from f and g which works no matter what f and g (and, for that matter, A and B) are. That fixed definition, of course, is the one of diagonalization, giving D a = g(f a a).

Cantor’s Theorem in its conventional form then follows from taking B to be the type of truth values and g the operation of negation; since g has no fixed points, it will follow that D cannot be in the range of f. Indefinability of satisfaction follows as above. But also, rather than focusing on such impossibility results, we can instead consider cases where f and g are such that f’s range must contain everything definable from f and g in an appropriately simple way, and then what the theorem gives us are fixed-point existence results; for example, versions of Kleene’s recursion theorem can be viewed through this lens as simple instances of Cantor’s result, as can the existence of fixed point combinators in the lambda calculus (the one that falls right out of Cantor’s proof would be the plain-vanilla Y combinator).

Kenny(14:39:54) :I didn’t fully work through what you said, but it sounds very similar to what I recall Andrej Bauer said here:

http://math.andrej.com/2007/04/08/on-a-proof-of-cantors-theorem/

Also, you can use latex code in WordPress blogs now (including the comments) just by enclosing the relevant stuff with dollar signs (as usual) as well as the word “latex” after the first dollar sign.

And thanks for pointing out the typo – I’ll fix it now.

John Ryskamp(09:58:59) :I see you haven’t read Garciadiego’s book on set theory yet. You will conclude from it, as I have, that Godel has no internally consistent grounds for relating truth to provability. His reference to Richard is particularly unfortunate. Unfortunate too is his footnote 8, a piece of nonsense which shows not only how dated his work is but also, what a poor scholar he was. Feferman et al. are also very skeptical of theorems–remarkably, they express this in their editorial notes to Godel’s works!

It’s too bad you are not aware of current research in the history of mathematics. You should educate yourself:

Ryskamp, John Henry, “Paradox, Natural Mathematics, Relativity and Twentieth-Century Ideas” (May 19, 2007). Available at SSRN: http://ssrn.com/abstract=897085

yetanothersheep(10:14:59) :The connection between diagonalization arguments and Gödels first incompleteness theorem was pointed out by Lawvere in:

Diagonal arguments and cartesian closed categories with author commentary

Lawvere uses category theory to formulate his result, but there´s an exposition not using category theory by Yanofsky:

A universal approach to self-referential paradoxes, incompleteness and fixed points

Both papers are freely available.