Hi John,

I’m doing a bit more research on the history of what you’ve called “The Astounding Theorem,” and I often call “The Fixed-Point Variant of the Diagonal Argument” or, more graphically, “The Scissor-Hinge Lemma.” According to the Wikipedia entry Cantor’s first uncountability proof, Cantor discovered the diagonal argument, his second proof of the uncountability of the reals, in 1877.

Visibly, self-application is a form of diagonalization, and the mathematical use of self-application seems to trace back to Richard’s Paradox, 1905. In that paradox we enumerate the properties of natural
numbers, and ask which properties do not apply to their own index, i.e., position in the enumeration. Such indexes are called “Richardians.” We then consider the index of the property of being a Richardian, with obviously paradoxical consequences.

Gödel’s incompleteness theorem (1931) is essentially a formalization of Richard’s paradox:

“To every omega-consistent recursive set K of formulae, there corresponds” a non-member of K whose negation is also non-member of K. [I copied this from the Wikipedia, but the portion outside the quotes omits some technical tedium. THP]

which simply says that the composition of K’s characteristic function with negation has a fixed point (which can’t be in the set because that would make the set inconsistent and thus omega-inconsistent). Of course, the K of interest was the set of provable formulae.

Note that Gödel already had a mathematical definition of “recursive set,” and that he obviously realized that it was a relevant definition of the notion of “effective computability.” This was five years before Church’s Thesis.

(For what follows my primary reference is the 2006 history of these matters, *The Logic of Curry and Church* by Jonathan Seldin.)

At the time both Church and Curry were working on theories of functions they hoped could serve as the foundation of mathematics. Obviously, Gödel’s result posed questions about their systems. But, Curry was at Penn State and had a huge teaching load and no graduate
students, Church was at Princeton and had Kleene and Rosser as graduate students, and he put them to work:

Next came Kleene’s dissertation [Kleene, 1935], which was based on Church’s definition of natural numbers. Kleene showed that Church’s system was adequate for the elementary theory of natural numbers by proving the third and fourth Peano axioms. In the course of doing this, he showed that a number of (recursive) functions could be represented as lambda-terms, including functions that Church had not thought could be represented that way. Rosser had also found some such representations in work that was never published, and by the fall of 1933, Church began to speculate that every function of positive integers that can be effectively calculated can be represented as a lambda-term. By early the following year, Church was convinced of what is now known as “Church’s Thesis.” See [Rosser, 1984, p. 334].

But meanwhile, in late 1934, Kleene and Rosser succeeded in proving that Church’s system of logic was inconsistent by showing that Richard’s paradox could be derived in it. [Kleene and Rosser, 1935]. Their proof also applied to the system of combinatory logic then being developed by Curry (see AS2.3 below).

Church, Kleene, and Rosser responded to this inconsistency by extracting from Church’s system of logic what is now called the pure lambda-calculus: the part of the system involving the formation of lambda-terms and the rules for reduction and conversion. In Church’s Thesis they already had an indication of the importance of pure lambda-calculus, and in the years following the discovery of the inconsistency, they obtained a number of major results, results which fully justified treating the pure lambda-calculus as a system on its own.

Per the Wikipedia:

One well-known (and perhaps the simplest) fixed point combinator in the untyped lambda calculus is called the Y combinator. It was discovered by Haskell B. Curry, and is defined as

$Y = \lambda f . ( \lambda x . f(x x) ) ( \lambda x . f(x x) )$

And, per Seldin: “Finally, [Curry] found a much simpler contradiction that could be derived under the assumptions of the Kleene-Rosser paradox in [Curry, 1942b].” I’m guessing that this 1942 work was
where Curry introduced this fixed-point combinator, but I’d like to know for sure.

Note that Kleene had already published his Recursion Theorem in 1938, which involved the same construction, but in the context of recursive-function theory. Almost surely, he and Rosser used it in replicating Gödel’s work (i.e., constructing Richard’s paradox) within
Church’s system of logic. And note that Seldin said that “Their proof also applied to the system of combinatory logic then being developed by Curry.” So, I’m betting that The Astounding Theorem appears in some form in:

S. C. Kleene and J. B. Rosser, The inconsistency of certain formal logics, *Annals of Mathematics* **36** (1935) 630-636.

Regards,

Tom

## Exercises

Test for zero:

If $n=0$ then $(x\mapsto F)$ is not applied to $T$, and the result is $T$; otherwise it maps $T\mapsto F\mapsto F \mapsto \cdots \mapsto F$ ($n$ times) and the result is $F$.

Decrement: Rather more complicated. The trick is to define a new function $g$ and new input $y$ in terms of $f$ and $x$ such that $g$ can distinguish the first application from the latter ones. So we turn the input into a pair consisting of a flag and the input. We unset the flag once we’ve applied the function. So let

and

Now define

where

and

Exponentiation: Note that we write $n(f)$ as $f^n$. Taking this literally, write

and