The Coq mailing list

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

Hi all,

This time, I have a problem to find a definition of the well-ordering
axiom (for all types, not just nat), aka Zermelo's theorem.

I cannot find a definition with only foralls and exists on the Web.

I made this:
  Axiom well_ordering : ∀ A,
    ∃ (R : A → A → Prop),
    ∀ P, (∃ x, P x) → ∃ ! y, P y ∧ ∀ z, P z → R y z.

Is it correct?

It seems not to be equivalent to the axiom of choice because the
"∀ ∃!" does not imply the existence of a function, since it is an
axiom (of unique choice), you told me (and I checked it in Coq
library).

All of this is because I am trying to make a formal proof of the
paradox of Banach-Tarski, well known to require the axiom of choice
and I am indeed at the point where I need one of its versions.

I need something to build the set (the type, actually) of all (what
they call) "orbits" on the surface of a sphere. With the above axiom
*and* the axiom of functional choice, I managed to prove that
   ∃ f : point → point, ∀ x y, same_orbit x y ↔ f x = f y.

I did it but since I use an axiom of my own, I am not sure I am
really allowed to do that.

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