[FOM] A question about AC in constructive mathematics

[Ben Sherman]

I think Andrej Bauer's MathOverflow answer (to essentially this question) does a good job of clarifying this:

https://mathoverflow.net/a/260473 <https://mathoverflow.net/a/260473>

> On Apr 28, 2018, at 8:35 PM, Kreinovich, Vladik <vladik at utep.edu> wrote:
> 
> FYI
> 
> -----Original Message-----
> From: fom-bounces at cs.nyu.edu [mailto:fom-bounces at cs.nyu.edu] On Behalf Of Arnon Avron
> Sent: Saturday, April 28, 2018 3:26 PM
> To: fom at cs.nyu.edu
> Cc: Arnon Avron <aa at tau.ac.il>
> Subject: [FOM] A question about AC in constructive mathematics
> 
> 
> 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
> https://cs.nyu.edu/mailman/listinfo/fom
> 
> -- 
> You received this message because you are subscribed to the Google Groups "constructivenews" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to constructivenews+unsubscribe at googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180428/e14f6f49/attachment.html>