Constructive logic and Russell's paradox To show that "naive set theory" doesn't work, Russell devised the famous example of the set $$A := \{ x \ | \ x  \not\in x \},$$ which turns out can't be a set after all, because either

*

*$A \in A$, but then by the property of all members of $A$ it follows that $A \not\in A$

*$A \not\in A$, but then again $A$ has to be a member of $A$, so $A \in A$.

Since both of these options yield a contradiction, $A$ can't be a set. But as I understand the whole premise of constructive logic is that it isn't valid to assume that either $A \in A$ or $A \not\in A$ has to hold.
On the other hand, by the above we have shown that $A \in A \iff A \not\in A$, which even in constructive logic can't hold.
So is Russell's paradox valid in constructive logic?

You can formulate the proof constructively as follows.  Suppose $A\in A$.  Then by definition of $A$, we conclude that $\neg(A\in A)$, which is a contradiction.  Since the assumption $A\in A$ led to a contradiction, we conclude $\neg(A\in A)$ (note that this is still valid constructively--constructively, $\neg p$ means the same thing as $p\rightarrow\bot$).
But now since $\neg(A\in A)$, the definition of $A$ implies that $A\in A$.  Thus we have reached a contradiction.
