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)

> 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 ($\lambda^{\to}$), 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").

<hr />

**Note:** 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.

<hr />

So $Y$ isn't typable in $\lambda^{\to}$, however, once you start expanding the type system, you eventually can give it a type!

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.

(I highly recommend [Types and Programming Languages](https://www.amazon.com/Types-Programming-Languages-MIT-Press/dp/0262162091) for more information on type theory and lambda calculus).

### Relating the $Y$-Combinator and incompleteness

<s>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.</s>

We will require the interpretation of the [Curry-Howard isomorphism](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence), that is:
* *types are propositions*
* *terms are proofs*

See [these notes](https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf) for more information.

Using the interpretation, we can consider the problem of [type inhabitation](https://en.wikipedia.org/wiki/Type_inhabitation): *given a type $T$ and a context $\Gamma$, does there exists a term $t$ such that $t$ has type $T$ in context $\Gamma$? The following is an important result: _[Type-inhabitability is PSPACE-Complete (and therefore decidable) in $\lambda^{\to}$.](https://en.wikipedia.org/wiki/Type_inhabitation)_ This would imply that every proposition corresponding to a type from $\lambda^{\to}$ would be either provable or disprovable.  (I'm not a logician, I hope the relevance to incompleteness is clear).

The $Y$-combinator is not typable in $\lambda^{\to}$, and hence it does not correspond to a proposition. Let's suppose that it were typable (in some other system), what proposition would it correspond to? It's actually rather difficult to say it, so I now am going to take from [Kunen's Set Theory](https://www.amazon.com/Introduction-Independence-Studies-Foundations-Mathematics/dp/0444868399) (1st edition, chapter 1, section 14):

> We may now state the basic result behind the Second Incompleteness Theorem and Tarski's theorem on undefinability of truth.

> If $\phi(x)$ is any formula in one free variable, $x$, then there is a sentence $\psi$ such that
> $$ \text{ZF} \vdash \psi \leftrightarrow \phi(\ulcorner \psi \urcorner). $$

> **Proof**

> Let $\sigma(v)$ be $\phi(v(\ulcorner v \urcorner))$. Then for each formula $\theta$ in one free variable,
> $$ \text{ZF} \vdash \sigma(\ulcorner \theta\urcorner ) \leftrightarrow \phi(\ulcorner \theta(\ulcorner\theta\urcorner) \urcorner). $$
> In particular,
> $$ \text{ZF} \vdash \sigma(\ulcorner\sigma\urcorner) \leftrightarrow \phi(\ulcorner \sigma(\ulcorner\sigma\urcorner) \urcorner), $$
> so let $\psi$ be the sentence $\sigma(\ulcorner\sigma\urcorner)$.

> The definition of $\sigma$ might require some additional explanation... 

...But please refer to the text for said *additional explanation*, it took me years to understand it.  (The definition of $\sigma$ is so confusing chatGPT didn't transcribe the image properly...)

**Finally,** hopefully, we can see the $Y$-combinator's manifestation in logic:

* The *type* of $Y$ **is** the lemma above
* The $Y$-combinator *itself* **is** proof of the above lemma

It makes sense: the proof above is an algorithm of sorts.  It takes as input a proposition in one free variable, and returns a sentence with a particular property.  The existence of this algorithm, AKA the $Y$-combinator, is the *basic result behind the Second Incompleteness Theorem and Tarski's theorem on undefinability of truth*.

Again:

- in $\lambda^{\to}$, the $Y$-combinator is not typable (is not a term in the language), and the propositions corresponding to its types are provable (either true or false).
- in other type systems including the $Y$-combinator, type inhabitation now becomes more difficult (undecidable in fact), and the existence of a proposition corresponding to it gives us the power to prove incompleteness.

### 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 pretty diagram from the paper:

$$\require{AMScd}\begin{CD}
1 @>a>> A \\
@V\langle a, c\rangle VV @VV\varphi V \\
A \times A @>>\operatorname{sat}> 2
\end{CD}$$

<hr />

Another approach is taken in: [Introduction to Turing categories](https://www.di.ens.fr/users/longo/files/Cockett-TuringCateg.pdf), where *Turing Categories* are a *convenient setting for the
categorical study of abstract notions of computability.*  Example diagram from paper:

$$
\begin{CD}
A^n @>>> A \\
@V{p \times 1}VV @VV{f}V \\
A \times A^n @>>> A
\end{CD}
$$

## Final Remark

I guess it's worth taking stock of everything and asking the original question: *what causes a formal system to be incomplete?*  If it truly does rest on the construction of the $Y$-combinator like I am sort of getting at, then it requires some basic constructions:

1. We need to be able to *duplicate information*
2. We need to be able to *name everything*
3. We need to be able to *evaluate procedures* given their *name* and the *name of their input*
4. We need to be able to *compose procedures*

## But what's the point?

What we gain from looking at this using the Curry-Howard correspondence, I suppose, is just another point of view -- another perspective.  When the question is about the *the true reason of the incompleteness of formal systems* and questions about type systems come up, it seems reasonable to point out the correspondence.  It's interesting to note that in computability theory, type theory, and logic, wherever the serious "problems" occur, you find the same diagonalization argument, which inevitably requires producing this $Y$.

Maybe $Y$ is the *true reason.*

  [1]: https://i.sstatic.net/6HgVEhJB.png