[FOM] A question about AC in constructive mathematics

[Chris Scambler]

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> 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
> https://cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180429/10ad0a1e/attachment.html>