Intuitively, how does one show Russell's paradox in intuionistic logic?

Question

I am reading the comprehension axiom wiki, where I find this interesting point:

Passing from classical logic to intuitionistic logic does not help, as the proof of Russell's paradox is intuitionistically valid.

How does one show that Russell's paradox works when we have no contradiction? The most simplest presentation that I understand involves the analogy involving a town with barber who shaves everyone who doesn't shave himself. The result arises from the contradiction, so I'd be interested on how to show this without the contradiction being allowed.

Answer 1

Intuitionistic logic does have contradiction! [1] It only lacks (some, but not all) instances of the law of excluded middle ($A \vee \neg A$) and double-negation elimination $\neg\neg A \rightarrow A$. In particular, you can prove $\neg A$ by assuming $A$, and reaching a contradiction using that assumption.

So a proof of Russell's paradox from unrestricted comprehension goes through as follows:

1. Consider the set $R$ so that $x \in R$ precisely if $x \not\in x$. This set exists by the axiom of unrestricted comprehension.
2. Assume for a contradiction that $R \in R$. From the definition of $R$ we know that if $x \in R$ then $x \not\in x$. Thus, if $R \in R$ then $R \not \in R$. But $R \in R$ by assumption, so we get $R \not \in R$, a contradiction.
3. Since assuming $R \in R$ led to a contradiction, we can conclude $R \not\in R$. From the definition of $R$ we know that if $x \not\in x$, then $x \in R$. But we already concluded $R \not\in R$, so $R \in R$ follows, a contradiction.

NB The proof above never uses double-negation elimination, nor does it use the law of excluded middle. So it's a valid proof according to intuitionistic logic (and according to usual classical logic as well). It is, however, not exactly the same as the usual proof of Russell's paradox given in introductory set theory textbooks. Those proofs tend to rely on the Law of Excluded Middle.

[1] Some particular proofs that people colloquially call "proof by contradiction" actually use double-negation elimination under the hood. They go something like this: "Assume $\neg A$. Then ..., which is a contradiction, so $\neg A$ is false, so $\neg \neg A$ holds. By double-negation elimination, $A$ itself holds." Such proofs are not intuitionistically valid, not because they rely on contradiction, but because they rely on double-negation elimination.