This cool observation is generalized in Lawvere's fixed point theorem[1]. It basically says that whenever you have an "interpreter" I : A -> (A -> B) that take

This cool observation is generalized in Lawvere's fixed point theorem[1]. It basically says that whenever you have an "interpreter" I : A -> (A -> B) that takes elements of A and turns them into functions A -> B, then if every such function is realized by some element of A (i.e., I is surjective) then any given function f : B -> B has a fixed point. The fixed point can be constructed by (1) letting q = \(a:A), f (I a a), which is a function A -> B, (2) letting p:A be something for which I p = q, then (3) letting s = I p p, which is the fixed point of f. For sets, the way Russell's paradox appears is this: letting Set be the class of all sets, then every set x determines a predicate, which is a function Set -> Bool that for each x returns true or false depending on whether or not y is an element of x. Have I : Set -> (Set -> Bool) be the function that takes a set and turns it into a predicate: I x = \y, y ∈ x. An axiom of set theory (extensionality) is that I is injective. What if I were also surjective? (This is the non-axiom "unrestricted comprehension", that every predicate determines a set.) Well, then we could apply the fixed point theorem to negation N : Bool -> Bool, but N obviously doesn't have a fixed point! (Using the above notation, q = \y, N (y ∈ y) is the predicate that checks whether a set doesn't contain itself, p = {y | N (y ∈ y)} is the supposed set of all sets that don't contain themselves, and s = (p ∈ p) is the impossible fixed point for N.) Here's what the theorem says for lambda calculus. Suppose L is the set of all lambda expressions (where equivalent lambda expressions are equal). In lambda calculus, every expression is also a function, in the sense that if E is an expression then \x, E x is equivalent, so we can have an "interpreter" I : E -> (E -> E) be the identity function. The fixed point theorem says that if you have a function f : L -> L, then it has a fixed point. And what is it? Tracing through the construction, we see it's nothing other than \x, (f x x) (f x x)! (The complexity in stating the theorem precisely is to be able to restrict what we mean by functions A -> B. For the lambda calculus example, we need E -> E to mean just the functions realizable as lambda expressions. This does work out because reflexive objects exist[2].) [1] https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theore... [2] https://ncatlab.org/nlab/show/reflexive+object https://ncatlab.org/nlab/show/reflexive+object