[FOM] A question about AC in constructive mathematics

Arnon Avron 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.


Arnon Avron

More information about the FOM mailing list