[FOM] A question about AC in constructive mathematics
sherman at csail.mit.edu
Sat Apr 28 23:40:25 EDT 2018
I think Andrej Bauer's MathOverflow answer (to essentially this question) does a good job of clarifying this:
> On Apr 28, 2018, at 8:35 PM, Kreinovich, Vladik <vladik at utep.edu> wrote:
> -----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.
> Arnon Avron
> FOM mailing list
> FOM at cs.nyu.edu
> 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...
More information about the FOM