Here is a reply that focuses on this part:
> The true source of the incompleteness attaching to all formal systems of mathematics, is to be found — as will be shown in Part II of this essay — in the fact that the formation of ever higher types can be continued into the transfinite ….
And some comments:
> And in what sense does the fact that we can strengthen a theory $T$ to a higher type system $T^+$ (in which we for example can prove that $T$ is consistent) cause the incompleteness of $T$? [Link](https://mathoverflow.net/posts/comments/627319_211169)
> I agree, and find it strange that Gödel asserted that this in fact causes incompleteness. Another question: Gödel said: "whereas in every formal system at most denumerably many types occur". How do you interpret this? [Link](https://mathoverflow.net/posts/comments/627555)
I just wanted to bring up a few interesting points, from lambda calculus / type theory and category theory.
### Observation from Lambda Calculus
So, there is a curious observation, namely that in the simply typed lambda calculus, you cannot type the $Y$-combinator:
$$ Y = \lambda f . (\lambda x . f x x) (\lambda x . f x x). $$
This turns out to be a symptom of one of virtues of the system: all typable expressions have normal forms (i.e. have "terminating computations").
However, once you start expanding the type system, you eventually can type the $Y$ combinator!
With $\mu$-recursive types:
$$ Y : \mu T . (T \to T) \to T. $$
And with parametric polymorphism (this may not be correct…):
$$ Y : \forall T . (T \to T) \to \forall T . (T \to T). $$
But, once you allow the $Y$ combinator to appear in your expressions, you get non-terminating computations, or more precisely, you can assign types to terms with no normal form.
A somewhat glib reading of Goedel, from the Curry–Howard correspondence, might consider the formation of *higher types* equivalent to allowing the recurive or polymorphic typed expressions into the language, and we would interpret *incompletness* as the fact that some terms have no normal forms (i.e. are non-terminating computations). In this case it should be more obvious how the higher type systems cause the incompleteness.
#### Side note on the $Y$-Combinator
This expression is a bit opaque, and it's not unique, but its main property is that:
$$ Y f = f (Y f). $$
That is, it allows us to calculate fixed points. These fixed points are crucial in the proof of Goedel's theorem and may appear something like:
For every formula in one free variable $\varphi$ there exists a sentence $\psi$ such that:
$$ \psi \iff \varphi ( \ulcorner \psi \urcorner ).$$
At least in Kunen's discussion of it, this is the primary result which is used to prove the non-definability of truth and eventually the second incompleteness theorem. The proof of this claim is just as ugly and confusing as the definition of the $Y$ combinator given above (it's in fact the exact same one).
### Relevant work from Category Theory
As far as the comment *whereas in every formal system at most denumerably many types occur*, I believe this is *leaking implementation details.* A big part of Goedel's proof is the (recursive) encoding of all formula into natural numbers, using prime decompositions to use them as a "handy" data structure. Eventually this allows the encoding of the notion of **provable** into the natural numbers, and at this point the game is lost, so to speak. The problem is that we can encode our formal system, then ask questions about it as if we were just asking questions about numbers, but by the way we've defined everything the answers about the numbers are equivalent to answers about the system. Perhaps "letting the systems ask questions about itself" is the "introduction of higher types" and is related to *denumerability* by the nature of we just enumerate all possible strings of symbols, assign them numbers in a reasonable way, then do stuff with them (made possible by the fact that anything we could possibly say comes from finite strings of a finite alphabet).
All of this seems like it needs to be abstracted away to let the mechanisms showcase themselves a bit more cleanly, and in the paper [*DIAGONAL ARGUMENTS AND CARTESIAN CLOSED CATEGORIES*](https://www.emis.de/journals/TAC/reprints/articles/15/tr15.pdf), Lawvere does this (he even includes a few hot takes…).
#### Here is a quick synopsis…
Basically he breaks down the problem into category theoretic terms, and demonstrates the main issue being the existence of a *weakly point-surjective morphism* leading to the ability to create a $Y$-combinator that forces fixed point properties on certain objects.
He goes on to weaken the hypotheses of Cartesian-Closedness to having finite products and a terminal object. The main demonstration here is that the ability to structure information need not be so strong: we can get away with projections and selection.
There is some rather technical material that I'm not smart enough to comment on extensively, but its basically continuing the development to arrive at some more elegant results (elegant from the point of view of category theory).
Finally the definition of truth and 1st incompleteness theorem are addressed. The important parts here are the construction of appropriate categories from theories and the idea of morphisms representing *equivalence classes of (tuples of) formulas or terms of the theory, where two formulas (or terms) are considered equivalent iff their logical equivalence (or equality) is provable in the theory*.
This construction is used to showcase a number of claims like *satisfiability is not definable*. This is the main result here, and the rest are building useful abstractions to capture the remaining notions.
The definition of $\operatorname{sat}$ is to relate some formula in one free variable $\varphi: A \to 2$ to some constant $c: 1 \to A$, and results in a pretty diagram:
$$\require{AMScd}\begin{CD}
1 @>a>> A \\
@V\langle a, c\rangle VV @VV\varphi V \\
A \times A @>>\operatorname{sat}> 2
\end{CD}$$
This diagram is related to the discussion of *weakly point-surjective morphisms* and leads to a fixed-point combinator (if such $\operatorname{sat}$ exists.) Again, most of the rest uses this result and extends it to other notions.
The last major generalization occurs with the introduction of $\operatorname{substitute}: A \times A \to A$ and of the *metamathematical* binary relations $\Gamma$, which satisfies:
For all $\varphi: A \to 2$ (formula in one free variable), there is a $c_\varphi: 1 \to A$ (a constant, i.e. the godel number), such that for all $a: 1 \to A$ (any "element" of $A$), we have:
$$ \operatorname{substitute}(c, a) \; \Gamma \; \varphi(a). $$
This is the abstraction of a lot of ugly work, and is meant to capture notions of provability and the like. It's actually quite impressive to see him capture the spirit with category theory so well. I've also read a bit about *Turing Categories*, but this paper I found to be the most satisfying thing I've read on the matter.
[1]: https://i.sstatic.net/6HgVEhJB.png