The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

On Thu, Nov 3, 2011 at 1:09 AM, Victor Porton 
<porton AT narod.ru>
 wrote:
> I'd like also the following statement either as an axiom or proved from
> other axioms:
>
> [[For every set S there exists x not in S]].
> (And maybe a more strong statements, I can't tell just now what exactly.)

As was already pointed out, you should formalize mathematics directly
in Coq, i.e., type theory, rather than on top of some formalization of
ZFC. You will suffer infinitely more if you try to do it
set-theoretically in Coq.

The statement "for every set S there exists x not in S" does not make
sense in type theory. In type theory a type has elements, but "x is an
element of type T" is not something that can be judged false, because
it is not a proposition but a typing judgment. (You are not supposed
to understand the previous sentence, yet.)

Anyhow, I guarantee to you that for every instance where you feel that
you need to produce an element which is not in a given set S, we will
be able to remove your need and tell you how to do what you want to do
in type theory.

I am attaching a little exercise in formalization of posets that shows
you how one might do this sort of thing (except that in a real example
you'd use setoids and possibly type classes).

With kind regards,

Andrej

Attachment: poset.v
Description: Binary data