Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Axiom of choice

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Axiom of choice


chronological Thread 
  • From: "Elnatan Reisner" <elnatan AT cs.umd.edu>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] Axiom of choice
  • Date: Wed, 27 Aug 2008 19:23:57 -0400 (EDT)
  • Importance: Normal
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.





Archive powered by MhonArc 2.6.16.

Top of Page