[FOM] A question about AC in constructive mathematics

[Richard Heck]

On 04/28/2018 05:26 PM, Arnon Avron 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.

I am not a specialist, but I will make a few remarks.

The result is not precisely stated. The theorem
    https://en.wikipedia.org/wiki/Diaconescu%27s_theorem
is that choice implies excluded middle *in certain sorts of constructive
set theories*.
AC does not imply LEM in intuitionistic number theory or analysis or in
Martin-Löf's
type theory.

Given the familiar fact that one person's ponens is another person's
tollens, one way
to understand the significance of this result is that there's something
wrong, from a
constructivist point of view, with the set theories in question. One
possible view is
that the extensionalizing move in constructive set theory is
wrong-headed from the
beginning and that what's needed is a more intensional treatment, such
as Martin-Löf's.
The axiom of extensionality is crucial to the proof that AC implies LEM,
and there is
no such axiom in intuitionistic type theory.

Presumably there are other responses, as well, that involve
modifications of the
constructive set theory in question. As far as Bishop goes, he was
apparently aware of
this result---it is an exercise  in his book---so one would suppose that
he had views about
its significance.

Riki Heck


-- 
-----------------------
Richard Kimberly Heck
Professor of Philosophy
Brown University

Pronouns: they/them/their

Website:         http://rkheck.frege.org/
Blog:            http://rikiheck.blogspot.com/
Amazon:          http://amazon.com/author/richardgheckjr
Google Scholar:  https://scholar.google.com/citations?user=QUKBG6EAAAAJ
ORCID:           http://orcid.org/0000-0002-2961-2663
Research Gate:   https://www.researchgate.net/profile/Richard_Heck