The Coq mailing list

["Dominique Larchey-Wendling" <dominique.larchey-wendling AT loria.fr>]

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/