[FOM] A question about AC in constructive mathematics

[Harvey Friedman]

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

Perhaps the most "paradoxical" case of this phenomenon would live in
intuitionistic arithmetic and is as follows?

There are arithmetic predicates P(i) and Q(i,j) such that

(for all i <= 1)(P(i) implies (there exists j <= 1)(Q(i,j))) implies
there exists f:{0,1} into {0,1} such that
(for all i <= 1)(P(i) implies Q(i,f(i)))

proves some bad LEM?

I'll leave this to subscribers to verify, extend, refine, etc.

Harvey Friedman