The Coq mailing list

[Victor Porton <porton AT narod.ru>]

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.)

 

I use something similar in my theory of generalizations: http://www.mathematics21.org/generalization.html (implemented in informal ZF and in Isabelle/ZF).

I want to make it in Coq also.

 

Suggestions welcome.

03.11.2011, 04:00, "Daniel Schepler" <dschepler AT gmail.com>:

2011/11/2 Victor Porton <porton AT narod.ru>

03.11.2011, 03:41, "Adam Chlipala" <adamc AT csail.mit.edu>:
> šVictor Porton wrote:
>> ššI am now studying Coq. I want to create a theory of posets, semilattices, lattices, and complete lattices.
>> ššI consider to base my theory on the above mentioned ZF modules.
> šI suggest thinking hard before trying to do Coq developments that look
> šlike ZF. šType theory is an _alternative_ to set theory, and it is much
> šmore convenient for the sorts of theorems I have experience with. šYou
> šmight find the same for your domain. šYou can easily work with sets
> š(e.g., ensembles in the Coq standard library) without bringing in ZF.

I need Zorn lemma. How to do it in Coq, except of the only way I know that is using a ZF formalization in Coq?

I proved the type-based version of Zorn's lemma in my ZornsLemma contrib (which isn't just about Zorn's lemma, but also has more general set-theoretic definitions and results, proved in a type theoretic context, such as finite types, countable types, etc.  It was enough to function as a foundation for a Topology contrib.)  It should be easy to find on the Coq contribs page.

I also have some basic results on filters, leading up to the existence of an ultrafilter extending any filter.  I don't recall whether I put those in ZornsLemma or Topology...
--
Daniel Schepler

--
Victor Porton - http://portonvictor.org