Kleene-Rosser paradox

https://en.wikipedia.org/wiki/Kleene-Rosser_paradox

The Kleene-Rosser paradox shows that certain systems of formal logic are inconsistent; in particular the version of Curry's combinatory logic introduced in 1930, and Church's original lambda calculus, introduced in 1932-33, both originally intended as systems of formal logic. The paradox was exhibited by Stephen Kleene and J. B. Rosser in 1935.

Kleene and Rosser were able to show that both systems are able to characterize and enumerate their provably total, definable number-theoretic functions, which enabled them to construct a term that essentially replicates the Richard paradox in formal language.

Curry later managed to identify the crucial ingredients of the calculi that allowed the construction of this paradox, and used this to construct a much simpler paradox, now known as Curry's paradox.