Qiaochu_Yuan comments on Godel's Completeness and Incompleteness Theorems - Less Wrong

34 Post author: Eliezer_Yudkowsky 25 December 2012 01:16AM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (85)

You are viewing a single comment's thread. Show more comments above.

Comment author: incariol 26 December 2012 06:06:31PM 2 points [-]

Given these recent logic-related posts, I'm curious how others "visualize" this part of math, e.g. what do you "see" when you try to understand Goedel's incompleteness theorem?

(And don't tell me it's kittens all the way down.)

Things like derivatives or convex functions are really easy in this regard, but when someone starts talking about models, proofs and formal systems, my mental paintbrush starts doing some pretty weird stuff. In addition to ordinary imagery like bubbles of half-imagined objects, there is also something machine-like in the concept of a formal system, for example, like it was imbued with a potential to produce a specific universe of various thingies in a larger multiverse (another mental image)...

Anyway, this is becoming quite hard to describe - and it's not all due to me being a non-native speaker, so... if anyone is prepared to share her mind's roundabouts, that would be really nice, but apart from that - is there a book, by a professional mathematician if possible, where one can find such revelations?

Comment author: Qiaochu_Yuan 27 December 2012 04:09:09AM *  9 points [-]

You can think of the technical heart of the incompleteness theorem as being a fixed point theorem. You want to write down a sentence G that asserts "theory T does not prove G." In other words, there is a function which takes as input a sentence S and outputs the sentence "theory T does not prove S," and you want to find a fixed point of this function. There is a general fixed point theorem due to Lawvere which implies that this function does in fact have a fixed point. It is a more general version of what Wikipedia calls the diagonal lemma. Interestingly, it implies Cantor's theorem, and one way to prove it proceeds essentially by constructing a more general version of the Y combinator. Yanofsky's A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points is a good reference.

I mention this for two reasons. First, there is a lot of visual machinery you can bring to bear on the general subject of fixed point theorems. For example, to visualize the Banach fixed point theorem you can think of a sequence of copies of the same shape nested in each other and shrinking towards a single point (the fixed point), and to visualize the Brouwer fixed point theorem you can draw a bunch of arrows in a disk.

Second, there is a graphical language, roughly analogous to Penrose graphical notation, for doing computations in Cartesian closed categories, and a version of Lawvere's theorem can be proven using this graphical language. Unfortunately I don't know a reference for this; I found the proof while trying to understand the Y combinator and don't actually know if it's in the literature (but it probably is).