In this note we will propose an informal analogy between Gödel's incompleteness theorem and the Y combinator as a way of gaining intuition into his approach.

Gödel devised a particularly clever way of creating a self-referential formula in first order logic. Newer presentations rely on diagonalization arguments, but it is still instructive and illuminating to delve into Gödel's original approach. It has renewed relevance in view of developments in modern programming languages.

Gödel wanted to create a formula along the following lines:

"This formula has the property that neither it nor its negation has a proof."

There is no direct way in first order arithmetic to express a notion of self-reference such as "this formula.."

Instead, Gödel came up with an "arithmetization" scheme, in which formulas in first order logic (i.e., syntactically well-formed finite sequences of symbols) could be mapped to natural numbers. With this trick, it becomes possible to reason within first-order arithmetic about these fancy numbers, and thereby to engage in formal reasoning about first-order formulas.

Consider the following two statements:

"There exists a formula with Gödel number M which possesses the property that neither the formula nor its negation has a proof."

"Oh, by the way. The Gödel number of the above formula is M."

The first formula by itself might be false; there might be no such number.

However, in combination with the second statement, things get interesting. If we were able to devise such a number "M", the formula would itself stand as a witness to the existence of a formula with the property that it asserts. So, we would be led to the conclusion that the formula is in fact true. On the assumption that first order arithmetic is consistent (no falsehood is provable), we have a formula that is true but not provable.

"M" in the above is an actual number. In the first statement, one has an arithmetic expression (i.e., a sequence of symbols such as "3 + 4*5 + 12^100000 + ...") that is short but that evaluates to a really large number.

After developing the idea of mapping formulas and proofs in first-order logic to integers, Gödel needed to use his new tool to come up with some way to express self reference. (The formula above has to have an embedded arithmetic expression "M" that unwraps and evaluates to the Gödel number of the entire formula.)

Gödel devised what we would today recognize as the Y combinator, expressed in first order arithmetic.

The essential similarity of the key trick in Gödel's incompleteness theorem and the Y combinator is a helpful way for those of us who are familiar with functional programming, Lisp, JavaScript, Python, etc. to gain intuition into the incompleteness result.

As an entry point, consider the standard lambda term with no normal form,

    (lambda x. (x x)) (lambda x. (x x))

It is possible to make the syntax a little bit more verbose, and have an expression that is legal python:

    (lambda x: (x(x))) (lambda x: (x(x)))

Now consider Gödel's arithmetic expression "Substitute(F, n)", which takes a number F, the Gödel number of a formula with a single free variable, and another number n. It simplifies to a number M which is the Gödel number of the formula F with n replacing all instances of its free variable.

(Defining this function "Substitute" was itself a major undertaking. One must code up a parser, implement something analogous to a symbol table, develop list data structures and bidirectional mappings between integers and lists of symbols, etc.)

One might interpret F (the first argument of "Substitute") as function-like, in the sense that for any number n, F [free_var := n] simplifies to some other number m.

Moreover, "Substitute(F, n)" acts like function application, taking a function F and an argument n and returning F(n). This is analogous to beta reduction in lambda calculus:

(lambda x. F(x)) (n)  ⇒  F[x := n]

So now consider "Substitute(F, F)", which is suggestive of "(x x)" in lambda notation.

Let M be the Gödel number of this formula, which has one free variable.

Finally, use an analogy to the above self-referential lambda term to create the formula G, defined as "Substitute(M, M)".

To what number does this arithmetic formula with no free variables simplify? The delightful answer is that it simplifies to its own Gödel number!

"M" is the Gödel number of "Substitute(x,x)", a formula with one free variable. If we substitute the number "M" for the two occurrences of the free variable "x", we get precisely "Subsitute(M, M)", the Gödel number of which is what is returned by the application of the "Substitute" function.

If we wanted to imitate the divergent behavior of the original formula in lambda calculus, we could do something like the following:

Given an integer M:

While possible:
    Decode M into its corresponding arithmetic expression.
    Simplify the expression to obtain an integer M'.
    Repeat the process with this new integer M'.

Just as it is a short step from the above simple self-referential lambda term to the Y combinator, so it is a short step from the above fact to the standard Gödel formula for which neither it nor its negation has a proof.

So, the above connection may be helpful in understanding the heart of Gödel's insight.

Here is the Y combinator. The only change from the above lambda term with no normal form is the introduction of a free variable "f".

    (lambda x. f(x x)) (lambda x. f(x x))

(We have omitted the abstraction on "f" and left "f" as a free variable for clarity. As above, it is easy to obfuscate the above formula a little bit and come up with a valid executable python version.)

The crucial difference is that every time we apply "beta reduction" or function application, we get the original term, but wrapped with "f":

    f((lambda x. f(x x)) (lambda x. f(x x)))

We can repeat this process as many times as we like:

    f(f(f(...f((lambda x. f(x x)) (lambda x. f(x x)))...)))

(This repeated unfolding is useful when using the Y combinator to work with recursion, but it turns out to be unnecessary for Gödel's argument; he just needed a single iteration to achieve his goal.)

Going back to our original goal, how might we construct the formula given at the top of this note? How do we construct a numerical constant "M" that makes the two assertions true?

We will abbreviate our hoped-for formula

"There exists a formula with Gödel number M which possesses the property that neither the formula nor its negation has a proof"

As follows:

f(M)

We start by replacing our placeholder "M" with a familiar looking expression,

    Substitute(x, x)

Here is the formula with that substitution.

"There exists a formula with Gödel number Substitute(x,x) which possesses the property that neither the formula nor its negation has a proof."

The above formula has a single free variable, "x".

Using our abbreviation, we can concisely express the above as:

f((x x))

As a well-formed syntactically valid formula in first-order logic, the above formula has a Gödel number; let's call its Gödel number "G".

Now, the coup de grace: We substitute the number G into our formula in place of the free variable "x":

"There exists a formula with Gödel number Substitute(G,G) which possesses the property that neither the formula nor its negation has a proof."

In terms of the abbreviated notation, this would become:

f(Substitute(f(x x), f(x x)))
             ^^^^^^  ^^^^^^

The highlighted sub-expressions above are instances of the Gödel number "G" defined above.

Now, consider the term

Substitute(f(x x), f(x x)).

Using our analogy of "Substitute()" in first order logic to beta-reduction in lambda calculus, this can be expressed as the clean-looking lambda term:

(f(x x)) (f(x x)).

If we turn the crank and perform the Substitute operation (or beta reduction), we get the following term:

f(f(x x) f(x x))

The nested arithmetic expression has "unwrapped" to become exactly the Gödel number of our original formula!

The number "G" is the Gödel number of a formula with a single free variable "x"; we can substitute any number into this formula in place of "x" using the Substitute function. In particular, it is completely reasonable to do so with the number "G". The resulting substitution yields precisely the Gödel number of our original formula.

So there we have it. We have used a version of the Y combinator expressed in first order predicate logic that allows us to create an expression that "unfolds" to the Gödel number of the formula that contains it as a sub-expression.