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
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
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").
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.
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 for more information on type theory and lambda calculus).
Relating the $Y$-Combinator and incompleteness
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.
See these notes for more information on the Curry-Howard
Remember from the Curry-Howard isomorphism that we interpret types as propositions, and an inhabitant of a type is a proof of the proposition, i.e., if a type is inhabitable, the corresponding proposition is provable. The following is an important result: Type-inhabitability is PSPACE-Complete (and therefore decidable) in $\lambda^{\to}$. 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 (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: it's this awful procedure, formalized as a propostion in the additional explanation. It takes as input a proposition in one free variable, and returns a sentence with a particular property. The existence of this $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, 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.
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:
- We need to be able to duplicate information
- We need to be able to name everything
- We need to be able to evaluate procedures given their name and the name of their input
- We need to be able to compose procedures
From the point of view of trying to describe formal systems in a metamathematical manner, it may be worth considering these requirements.