The Coq mailing list

[Thomas Payne <thp AT cs.ucr.edu>]

In set theory without urelements, per the axiom of extensionality, the 
content of a singleton is its interstection, which is equal to its union.


On 9/11/16 9:33 AM, Daniel de Rauglaudre wrote:
> When I said "false", I was talking about the fact that it was provable.
>
> On Sun, Sep 11, 2016 at 05:40:14PM +0200, Dominique Larchey-Wendling wrote:
> > Well it is not provable in Coq. But it is not false ...
> >
> > Envoyé avec AquaMail pour Android
> > http://www.aqua-mail.com
> >
> >
> > Le 11 septembre 2016 11:35:57 Daniel de Rauglaudre
> > <daniel.de_rauglaudre AT inria.fr>
> >  a écrit :
> >
> > > Ah indeed, axiom of unique choice... thanks. It is because somebody
> > > told me the choice was computable in that case but I could not prove
> > > it. Normal, if it is false :-)
> > >
> > > On Sun, Sep 11, 2016 at 11:22:25AM +0200, Dominique Larchey-Wendling wrote:
> > > > I think it is called reification in Coq. And yes it is the axiom of
> > > > unique choice... The relation does not contain enough information to
> > > > compute the value. Unless P is decidable and the type is enumerable
> > > > of course.
> > > >
> > > > Envoyé avec AquaMail pour Android
> > > > http://www.aqua-mail.com
> > > >
> > > >
> > > > Le 11 septembre 2016 11:09:23 Daniel de Rauglaudre
> > > > <daniel.de_rauglaudre AT inria.fr>
> > > >  a écrit :
> > > >
> > > > > Hi all,
> > > > >
> > > > > Is the axiom of choice required if all sets have one only element ?
> > > > > If not, how to prove it ?
> > > > >
> > > > > Russel said that if all sets contain a pair of socks, we need the axiom
> > > > > of choice to select a sock in each pair but that if they are shoes,
> > > > > we don't need it, because the choice function can be : "take the left
> > > > > shoe".
> > > > >
> > > > > But for sets of one only element ?
> > > > >
> > > > > Namely, I want to prove :
> > > > >    (∀ x, ∃! y, P x y) → ∃ f, ∀ x, P x (f x)
> > > > >
> > > > > Is is possible, or do I need the fucking axiom of choice ?
> > > > >
> > > > > Thanks.
> > > > >
> > > > > --
> > > > > Daniel de Rauglaudre
> > > > > http://pauillac.inria.fr/~ddr/
> > > --
> > > Daniel de Rauglaudre
> > > http://pauillac.inria.fr/~ddr/