The Coq mailing list

[Andrej Bauer <Andrej.Bauer AT andrej.com>]

It is perhaps worth thinking about the axiom of choice, even on this
list, outside of the context of Coq.

There are many formulations of "constructive logic" or "constructive
mathematics", such as:
- type theory a la Martin-Lof
- first-order intuitionistic logic + (Heyting) arithmetic
- first-order intuitionistic logic + constructive set theory
- higher-order intuitionistic logic (topos theory)

There are several possible formulations of choice. I will concentrate on
the one that says that every total relation has a choice function (it is
called AC_fun in Coq.Logic.ChoiceFacts, another one is AC_rel).

The axiom of choice is typically not valid in any constructive setting
in which:
(a) functions A -> B obey the law of extentionality

    forall f, g : A -> B,
      f = g <-> forall x : A, f x = g x.

(b) and proofs of forall-exists statements need not preserve
equality, i.e., a proof p of

   forall x : A, exists y : B, phi x y

need not satisfy the condition

   forall x y : A, x = y -> p x = p y.

There may be some discussion about what the = sign means.

Type theory satisfies (b) but not (a), and you can prove a
type-theoretic version of choice (just like Elnatan did). A
"mathematical" axiom of choice would be expressed in Coq using setoids,
and it would say that every proof of

  forall x : A, exists y : B, phi x y

gives a function A -> B which respects the equivalence relations on A
and B. This of course cannot be proved, but it is what mathematicians
call axiom of choice (and is the useful version in mathematics, when
setoids or some equivalent are present).

In general, a setting which separates logic and type theory will fail to
prove axiom of choice. This is visible in Coq which distinguishes
between Set and Prop.

This version of choice is provable (because we do everything in Set):

Theorem choice1:
  forall A B : Set,
  forall phi : A -> B -> Set,
  (forall x : A, { y : B & phi x y }) ->
  {f : A -> B  & forall x : A, phi x (f x)}.

But this version is not provable, because we use the existential that
maps into Prop:

Theorem choice2:
  forall A B : Set,
  forall phi : A -> B -> Prop,
  forall x : A, ex (phi x) ->
  ex (fun f : A -> B => forall x : A, phi x (f x)).

I hope I got the examples right.

Best regards,

Andrej