[FOM] A question about AC in constructive mathematics
Harvey Friedman
hmflogic at gmail.com
Mon Apr 30 03:09:57 EDT 2018
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
More information about the FOM
mailing list