[FOM] A question about AC in constructive mathematics
aa at tau.ac.il
Sat Apr 28 17:26:06 EDT 2018
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.
More information about the FOM