Russell's paradox and the Y combinator (opens in new tab)

It might be valuable to expand the definitions of things a bit.

First, we talk about characteristic functions. As noted, they are merely functions which return either 1 or 0, True or False. They represent sets by examining their argument and returning True if and only if the set they represent contains that thing.

So, if x is a characteristic function and (x x) is True, then x "contains" itself. Then N is just negation, so if N (x x) is True then x does not "contain" itself. That much is simple.

Now we form a special new characteristic function, R, defined as

    R x = N (x x)

When is (R x) True? Exactly when x is "contained" in R. When does that happen? When N (x x), e.g., when x does not "contain" itself.

So this is a well-defined characteristic function and therefore represents what we might think is a well-defined set.

But what happens when we check (R R), i.e. to see if R contains itself?

Well, R, by definition, contains all things which are not members of themselves. If R is in R then (R R) is True, but then N (R R) is False and (R R) = False. Contradiction!

We can inline R into (R R) in order to take a look at the functional form.

    (\x -> N (x x)) (\x -> N (x x))

and the author notes that this is the same form as the Y-combinator with its first argument specialized to N.

    Y f = (\x -> f (x x)) (\x -> f (x x))
    Y N = R R

And there we go!

I'm not a native speaker, I'm sorry you had trouble going through it. I tried to keep it short but maybe did not articulate the first paragraph and the end of the second ideally.

Hopefully, you understood the core idea.

You were potentially not in the intended audience.

Actually, the connection between non-terminating computations and Russell's paradox is fairly strong. The piece of explanation missing from the article that is that the naive conception of sets corresponds to total boolean valued functions. That is, a set is a rule that answers whether a value is in the set or not. To get set theory out of lambdas, you just have to restrict to the subset of lambdas that only apply sets to sets and that end up returning a proposition.

So you'd have to reject a lambda like this: λx. x (x x), because when you rewrite that in set theory notation it looks like this: { x | x ∈ (x ∈ x) }. Bad since (x ∈ x) is a proposition used as a set. We'd also reject λx. x because it returns a set and not a proposition. Labeling expressions with one of two sorts (proposition or set) can be done statically, though, and this allows us to quickly check whether a lambda corresponds to a construction of naive set theory. Once you have this correspondence, the rest of the author's note goes through fairly well.

Except that technically Y = λN. R R, not R R.

It also took someone until the mid-20th century to formalize the Y combinator, though... Earliness of discovery is no grounds on which to consider the Y combinator less "deep" than Russell's paradox (if anything, the reverse!).

It's true! The reasoning is fairly simple, though.

In such a language, types classify terms and types correspond to theorems. The type/theorem for a fixed point is

    fix : forall a . (a -> a) -> a

which as a theorem reads: "for any proposition A, if we can prove 'if A, then A' then we can prove A". Hopefully it's now clear why having 'fix' in your prover language won't work!

Correct. One way to think of it is that running the program produces a proof of the theorem. But since the program is guaranteed to terminate with a proof (since all functions are total in Coq), why run it at all? Type checking is sufficient.