[FOM] A question about AC in constructive mathematics
cscambler at gmail.com
Sat Apr 28 23:33:44 EDT 2018
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.
> Arnon Avron
> FOM mailing list
> FOM at cs.nyu.edu
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the FOM