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

[Robert Black]

[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>