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).
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).