The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

On 2013/10/28 t x 
<txrev319 AT gmail.com>
 wrote:
> Paradox with "sets of sets":
>   X = { s | s \not\in s }
>
> In classical logic, there's the argument:
>   does X \in X?
>     if yes, then X \not\in X, contradiction
>     if not, then X \in X, contradiction

You don’t need to use excluded middle for that, you also get a
contradiction constructively:

Assume X \in X. Then, by definition we have X \not\in X, hence we have
a contradiction. This shows that X \not\in X.
Hence, by definition, X \in X : contradiction.

Guillaume