The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Thorsten Altenkirch wrote:
> I would like to encode Russell's paradox in Coq for my class, or more 
> precisely Thierry's version of it (the paradox of trees). But how do I 
> assume tat there is a set of all sets, or Set : Set?

You could always do a deep embedding of just the features of ZF needed 
for your example.

It seems kind of ironic that it ends up being inconvenient not to be 
able to apply inconsistent reasoning in Coq. ;)