The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

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/
> 

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/