The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Elnatan Reisner wrote:
> Can someone shed some light on this contradiction? Are some forms of the
> axiom of choice provable and others not?
>   

In constructive logic, certain statements of the axiom of choice are 
trivial, since proofs of existence give effective methods for computing 
the things that exist.

One big source of confusion here is the [Prop]/[Set] distinction in Coq, 
which has no counterpart in almost any other formal system, least of all 
set theory, where proofs are considered to exist in some separate 
magical universe.  To (A) make extraction effective and (B) avoid 
surprising consequences of impredicativity, Coq imposes serious 
elimination restrictions on [Prop], which enforce lack of "information 
flow" from proofs to programs.  One statement of AC in Coq is 
essentially a controlled way of casting from existential packages in 
[Prop] to their counterparts in [Set].  Such an axiom is interesting for 
a completely different reason than AC is interesting in ZF; the 
"philosophical commitments" that the two axioms propose are completely 
disjoint, as far as I understand.

You can find a slew of variants of AC in the Logic.ChoiceFacts module.  
Further dimensions of variation that are interesting in Coq include 
converting relations to functions and statements about how there exist 
unique elements satisfying relations.

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

Well, the type hierarchy makes the analogy wrong, IMO. ;)

> and I
> imagine reading [x : A] as 'x is an element of A'. Does it make sense to
> think of things this way?

Yes and no.  It can be a reasonable source of intuitions, but you just 
won't find any way to reify type membership as a proposition in the way 
you are probably hoping to.

> 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].
>   

Neither of these conventions accomplishes anything logically.  Terms 
have types intrinsically in Coq; you don't need to state propositions to 
impose such constraints.  Sometimes you want to "inject" a non-[Prop] 
term into [Prop] with a type family like the standard library's 
[inhabited], but this has no deep interpretation in the standard, 
set-theoretical view of the world.

I think what you are discovering, with your difficulties crafting a 
satisfying statement of AC, is that the elements of AC-stated-for-ZF 
that you think of as critical are actually barely worth saying in 
constructive logic.  You need one or more of the "gimmicks" of the later 
versions of AC from Logic.ChoiceFacts for things to get interesting in 
that kind of way.