The Coq mailing list

["Elnatan Reisner" <elnatan AT cs.umd.edu>]

A little while ago, I heard someone say that the axiom of choice is
provable in constructive logic. But there are some examples of the axiom
of choice implying excluded-middle linked from the Coq website; for
example:

http://coq.inria.fr/library/Coq.Logic.Diaconescu.html
http://coq.inria.fr/contribs/paradoxes.html

These definitions don't correspond to the way I usually think about the
axiom of choice, though. (But maybe I don't think about it enough to know
all of its different flavors.)

Can someone shed some light on this contradiction? Are some forms of the
axiom of choice provable and others not?

To throw my hat in the ring, below is something that I think would qualify
as an 'axiom' of choice that you can prove in Coq.

I'm sort of imagining that Coq's [Type] is analogous to the verboten
set-of-all-sets (hoping that the type hierarchy makes this okay), and I
imagine reading [x : A] as 'x is an element of A'. Does it make sense to
think of things this way? And if so, is there a way better to say that
something is in a particular type? Below, I write
{x : F a | True}
to mean that [F a] is nonempty, and
exists x : F a, f a = x
to mean that [f a] is in [F a].

Thanks for any thoughts.

-Elnatan


Lemma choice :
  forall (A : Type) (F : A -> Type), (* For any family [F] of types *)
  (forall a, {x : F a | True}) ->    (* which are all inhabited, *)
  exists f, forall a, exists x : F a, f a = x.
(* there is a function [f] which, for every index [a],
   yields a value in [F a] *)
Proof.
  intros A F H.
  exists (fun a => match (H a) with exist fa _ => fa end).
  intro a. esplit. auto.
Qed.