[FOM] A question about AC in constructive mathematics
Berger U.
u.berger at swansea.ac.uk
Sun Apr 29 07:58:50 EDT 2018
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
More information about the FOM
mailing list