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?
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).
Thinking about algebra (e.g. group theory) makes a lot of this make more sense. The definition of a group is a “theory”; any particular group is a “model”. This isn’t a huge revelation or anything, but it’s easier to think about these ideas in the context of algebra (where different structures that behave similarly are commonplace) rather than arithmetic (where we like thinking about one “true” picture).
Here’s how I visualize Goedel’s incompleteness theorem (I’m not sure how “visual” this is, but bear with me): I imagine the Goedel construction over the axioms of first-order Peano arithmetic. Clearly, in the standard model, the Goedel sentence is true, so we add G to the axioms. Now we construct G’ a Goedel sentence in this new set, and add G″ as an axiom. We go on and on, G‴, etc. Luckily that construction is computable, so we add G^w as a Goedel sentence in this new set. We continue on and on, until we reach the first uncomputable countable ordinal, at which point we stop, because we have an uncomputable axiom set. Note that Goedel is fine with that—you can have a complete first-order Peano arithmetic (it would have non-standard models, but it would be complete!) -- as long as you are willing to live with the fact that you cannot know if something is a proof or not with a mere machine (and yes, Virginia, humans are also mere machines).
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?
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).
Visual/imaginative modelling of mathematical tasks is not a universal trait.
However, it’s a useful skill.
Thinking about algebra (e.g. group theory) makes a lot of this make more sense. The definition of a group is a “theory”; any particular group is a “model”. This isn’t a huge revelation or anything, but it’s easier to think about these ideas in the context of algebra (where different structures that behave similarly are commonplace) rather than arithmetic (where we like thinking about one “true” picture).
Here’s how I visualize Goedel’s incompleteness theorem (I’m not sure how “visual” this is, but bear with me): I imagine the Goedel construction over the axioms of first-order Peano arithmetic. Clearly, in the standard model, the Goedel sentence is true, so we add G to the axioms. Now we construct G’ a Goedel sentence in this new set, and add G″ as an axiom. We go on and on, G‴, etc. Luckily that construction is computable, so we add G^w as a Goedel sentence in this new set. We continue on and on, until we reach the first uncomputable countable ordinal, at which point we stop, because we have an uncomputable axiom set. Note that Goedel is fine with that—you can have a complete first-order Peano arithmetic (it would have non-standard models, but it would be complete!) -- as long as you are willing to live with the fact that you cannot know if something is a proof or not with a mere machine (and yes, Virginia, humans are also mere machines).