[FOM] A question about AC in constructive mathematics

[Berger U.]

The reason for the mismatch of set-theoretic AC and type-theoretic AC
(even for choice out of a 2 element set) is that in type-theoretic AC 
(which is in fact a theorem of type theory) the choice function 
may depend on proofs while this is not the case in set-theoretic AC.

Below I repeat the proof of LEM using set-theoretic AC
and try to explain the mismatch in more detail.

In IZF: 

Let P be a proposition. By separation we can define

A = {x in {0,1} | x = 0 or P}
B = {x in {0,1} | x = 1 or P}

X = {A,B} (by pairing)

Since A and B are both nonempty (0 in A, 1 in B),
by set-theoretic AC there is a function f : X -> bigunion X
such that f(A) in A and f(B) in B, in particular  
f(A), f(B) are both in {0,1}.

Since equality on {0,1} is decidable 
(i.e. forall x,y in {0,1} (x = y or x =/= y) is provable),
we can do a case analysis on f(A) = f(B) or f(A) =/= f(B):

(1) If f(A) = f(B) one easily sees that P holds 
(sub case analysis on f(A) = 0 or f(A) = 1).

(2) If f(A) =/= f(B) then A =/= B, by extensionality. Hence not P
(the assumptions P leads to a contradiction).

Hence P or not P.

Explanation why set-theoretic AC is NOT the translation of 
type-theoretic AC into set theory and hence the argument above
does not prove LEM in IZF + type-theoretic AC:

In the situation above we have 

forall u (u in X -> exists y (y in u))

By type-theoretic AC, there exists a function f that maps
any u and any proof p of 'u in X' to a pair f(u)(p) = (y,q)
where q is a proof of 'y in u'.

Now we see why the argument in (2) fails: from f(A)(p1) =/= f(B)(p2)
one can only conclude (A,p1) =/= (B,p2). It may well be that A = B
but p1 =/= p2. For example, p1 can be obtained from a proof of '0 in A' 
while p2 is obtained from a proof of P. So, it is wrong to conclude not P.

Functions depending on proofs are sometimes called 'intensional' or 'methods'.

I recommend

https://plato.stanford.edu/entries/axiom-choice/choice-and-type-theory.html

At the end of that article there is a hint that Maietti's  
propositions-as-monotypes interpretation is a way to resolve the mismatch.

Ulrich Berger





________________________________________
From: fom-bounces at cs.nyu.edu [fom-bounces at cs.nyu.edu] on behalf of Chris Scambler [cscambler at gmail.com]
Sent: 29 April 2018 04:33
To: Foundations of Mathematics
Cc: Arnon Avron
Subject: Re: [FOM] A question about AC in constructive mathematics

I also have a related question: the proof of ac--> lem uses choice on a 2 element set. But choice for finite sets is probable by an apparently constructive argument. I've never quite understood how these are reconciled--- thoughts from the cognoscenti most welcome!

On Sat, Apr 28, 2018, 9:33 PM Arnon Avron <aa at tau.ac.il<mailto:aa at tau.ac.il>> wrote:

Recently I came across a theorem (and a proof) that
AC implies the law of excluded middle in constructive
mathematics, implying that AC should be rejected
by intuitionists. I was surprised, since AC seems to me
to be valid according to the BHK interpretation of the
logical constants, and is a indeed a theorem in Martin-Lö's
intuitionistic type theoy.  Also Bishop wrote in his book
that AC is valid from a constructive point of view.

 I'll be very grateful if one of the specialists here on FOM
clarifies this issue for me.

Thanks,

Arnon Avron
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu<mailto:FOM at cs.nyu.edu>
https://cs.nyu.edu/mailman/listinfo/fom