# [FOM] Fwd: Re: A question about AC in constructive mathematics

Robert Black mongre at gmx.de
Sun Apr 29 11:51:53 EDT 2018

```[I've corrected a typo]

Arnon's question puzzled me at first too, but here's a short version of
the answer (pasted from an introduction to the Philosophy of Mathematics
that I'm writing; apologies for the remaining flavour of Latex):

The use of choice by the classical mathematician to prove the existence
of undefinable sets or functions is of course nonconstructive,
but_inside_ constructivist mathematics a version of choice is valid, namely

(\forall x in N)(\exists y in Y)phi(x,y) -> (\exists f: N->Y)(forall x
in N) phi(x,f(x)).

The reason is that a constructive proof of (\forall x in N)(\exists y in
Y)phi(x,y) consists precisely in providing such a function. It is
natural to think that this will now generalize to _any_ domains:

(\forall x in X)(\exists y in Y)phi(x,y) -> (\exists f: X->Y)(forall x
in X) phi(x,f(x)),

but it won't. The reason is that the function provided by the proof of
\forall x\exists y may not respect the identity defined on the domain X.
(Remember: N is special, because identity on N is decidable.) Indeed a
simple example shows that were we to admit choice in this more general
form we could prove the law of excluded middle. Let A be any proposition
whatever and define the two sets a = {z | z=0 v (A & z=1)} and b = {z |
z =1 v (A & z=0)}. Obviously (\forall x in{a,b})(\exists y in N) y in x,
but a corresponding choice function f would (as is easily seen)* be such
that f(a)=f(b) iff A, and since f(a)=f(b) v f(a) ≠ f(b) (f is supposed
to constructively produce a natural number from each of a and b and
remember again: identity on N is decidable) we would have A v not-A.

*If A is true then a=b and so f(a)=f(b), and if f(a)=f(b) then a and b
must have a member in common, which is only possible if A is true.

Robert Black

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180429/4f3a6832/attachment-0001.html>
```