[FOM] A question about AC in constructive mathematics

[Colin McLarty]

I think the disconnect is best seen as being this: The theorem that AC
implies the law of excluded middle holds in settings like topos theory and
Intuitionistic Zermelo Frankel, which are intuitionistic only in the formal
sense of limiting excluded middle.

In these settings a function or a subset need not be computable to exist.
Computability is just not a requirement.  And so in these settings AC is a
much more sweeping claim.  Indeed in the Brouwerian or BHK setting AC is
such a narrow claim that it is demonstrable.

Colin

On Sat, Apr 28, 2018 at 5:26 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/d766a838/attachment-0001.html>