The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

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.