Axiom of choice

[Elnatan Reisner]

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.

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Adam Chlipala-3]

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.

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Andrej Bauer]

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

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Andrej Bauer]

Andrej Bauer wrote:
> 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.

I forgot to point out what the difference between Set and Prop is: the
latter has proof irrelevance. Coq achieves proof irrelevance by imposing
restrictions on maps from Prop to Set.

Andrej

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Thorsten Altenkirch]

Hi Andrej,

while everything you say seems correct, I think, I disagree with the  
gist of it. Per Martin-Loef offered a similar explanation - but then I  
was never too impressed by authority... :-)

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

Indeed.

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

I don't agree. This "problem" only arises because you are using  
setoids to represent equality. In my view any construction should  
preserve equality, which is what we mean by "equal"! Moreover, it  
would be misleading to imply hat there as an issue with  
extensionality, Extensionality only exposes the flaw in (b).

I'd like to offer another analysis: the issues with the axiom of  
choice only arise if we say "A", i.e. accept constructive principles  
but don't say "B", i.e. use Type Theory to distinguish between Set and  
Prop.

The type-theoretic version of the existential, the Sigma type, does  
not live within Prop. I.e. given a set A and a predicate P : A ->  
Prop, it is not the case that Sigma a:A,P a : Prop. On the other hand,  
because Sigma a:A,P a Set we can project out the witness.

If we want to stay within Prop, i.e. restrict ourselves to logic, we  
have to give up this possibility. E.g. this can be achieved by using  
boxes (in the sense of your paper with Steve Awodey). I.e. we can define

        exists a:A,P a = [Sigma a:A,P a] : Prop

Once, we do this, there is absolutely no reason why we should accept

        f : forall a:A,[Sigma b:A, R a b]
        ------------------------------------------------------------
        ac_prop f : [Sigma f : A -> A, forall a:A, R a b]

for an arbitrary A. And indeed Diaconescu's construction shows that we  
can choose A, s.t. ac_prop implies the excuded middle (in Prop, i.e.  
[Q \/ not Q]).

It seems to me that the propositional axiom of choice (ac_prop) is the  
consequence of a certain indeciseveness: once we use the box, we have  
given up the right to expose the witness - indeed the box is a black  
one. But then we change our mind and say, actually after all I'd like  
to use the witness for a construction.

As I have already indicated, there are cases where ac_prop can be  
justified, e.. if A=Nat. This is a consequence that if A is a trivial  
setoid then the interpretation of f in the setoid model already  
contains the choice function we need to prove the conclusions. Since  
this construction works for any trivial setoid, it applies to any Type  
which doesn't contain quotients (using extensional or observation Type  
Theory). Diaconescu's construction on the other hand leads to a setoid  
A which is highly non-trivial.

Since this is the Coq mailing list, I'd like to remark that I think it  
is a shame that Coq while originally based on Type Theory is used in a  
way which strictly separates sets and propositions. This has historic  
reasons but I think it is time to move on.

Cheers,
Thorsten

P.S. I have copied in Bas, who may have better things to do then to  
follow the Coq mailing list, since I had a number of related  
discussions with him.

>
> 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
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club