The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Regarding the shoe analogy, just being different doesn't imply that one can distinguish, let alone select one of them.

Analogies aside, you may want to ditch Prop and switch to Type for your logical needs. Then you can easily prove what you want.

To switch, the notations ∧ , ∨ , ∃ will need to be redefined to use prod, sum, and sigT respectively.

I should warn that Coq's logic-related tactics are often hard coded for Prop -- at least they were 3-4 years ago.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sun, Sep 11, 2016 at 5:09 AM, Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr> wrote:

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/