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 = (\lambda f : T \to T) \big( (\lambda x: \mu A . A \to T). f (x x) \big) \big( (\lambda x: \mu A . A \to T). f (x x) \big) : (T \to T) \to T$$
Note that the $\mu$ types appear in the typing of the inner terms. In type systems that interpret $\forall$ such as with parametric polymorphism ($\lambda P$) or dependent types ($\lambda \omega$) $Y$ can get a type as well, but the important point of this is addressed later (see Lambda Cube for a discussion of these type systems).
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.
We will require the interpretation of the Curry-Howard isomorphism, that is:
- types are propositions
- terms are proofs
See these notes for more information.
Using the interpretation, we can consider the problem of 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}$. 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:
- 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.
Relating the type of the $Y$-combinator and Godel's claim
Recall the claim that:
The true source of the incompleteness, is to be found ... in the fact that the formation of ever higher types can be continued into the transfinite
In type theory, the formation of ever higher types would correspond to using a type constructor, i.e. in $\lambda^{\to}$ that would be '$\to$.' For example, given types $A$ and $B$, we form the type $A \to B$, written more obscurely as $\to(A, B)$. When dealing with types mathematically, especially when considering recursive types, it can be convenient to think of types as trees, as demonstrated by this figure from Pierce's book:
In this figure, the labels 1 and 2 are just labels to identify positions and arity, and Top is some given base type (typically a type inhabited by a single element, like $\{\cdot\}$ or x = x - that these types exist and are inhabited are some axioms of the system). The type on the right of the figure is in fact an infinite type, as is hinted by the ellipsis. In $\mu$ notation it would be written:
$$ \mu T . \mathrm{Top} \to T $$
This can be interpreted as an (extended) equation:
$$ T = \mathrm{Top} \to T = \mathrm{Top} \to (\mathrm{Top} \to T) = \mathrm{Top} \to (\mathrm{Top} \to (\mathrm{Top} \to T))$$
(Here we get the continued equation by substituting the definition of $T$ for $T$ over and over again.)
This same procedure of unfolding the type definition from $\mu$ can be repeated with the inner types of the $Y$-combinator, revealing that there is an infinite type. Recall the type of the parameter of the inner term of $Y$:
$$ \mu A . A \to T$$
This is nearly the same as the infinite type shown above, but instead of "extending to the right" it will "extend to the left."
Unfortunately, $\mu$ doesn't correspond so nicely to logic. In other type systems, in particular when we have parametric polymorphism or dependent types, we need to interpret the $\forall$ symbol. But this is where the infinite type is hidden in these systems. In the notes above, $\forall$ is interpreted as an (transfinite) product, while in other systems it is interpreted as a natural transformation (see Bartosz Milewski's discussion of natural transformations in Category Theory for Programmers). In either case, we get infinite types if there is an infinite number of types.
The idea here is that when we can interpret:
$$ \forall x \phi(x) = \phi(x_1) \land \phi(x_2) \land \phi(x_3) ... $$
Where $x_1, x_2$ is an enumeration of all members of the domain. Don't ask what if the members aren't enumerable?, it's not relevant.
To truly wrap up Godel's claim we would need to show that any such extension to infinite types would lead to a typing of $Y$ and hence a valid proof of the diagonalization lemma (which, taking Kunen's lead, we'll assume is sufficient to prove incompleteness). I'm not prepared to really make this claim without making some further assumptions on the formal system. I bet if we assume that the formation of terms is defined inductively (or co-inductively), and composition is found somewhere, then something could be shown.
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 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}$$
Another approach is taken in: Introduction to Turing categories, 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:
- 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
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.
