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

[Mummert, Carl]

I don't think that Martin-Löf's 2009 paper "100 Years of Zermelo’s Axiom of Choice: What was the Problem with It?" [1] has been mentioned yet in this thread.  

There is also a nuance about Diaconescu's theorem - there is more to it than just the lack of decidability of equality on the domain. In constructive Heyting arithmetic in all finite types (E-HA^\omega), only equality for numbers is decidable - even equality for type 0->0 is already undecidable. But nevertheless we have the axiom of choice for every finite type and every formula, constructively:

AC(\sigma,\tau):   [ (\forall x^\sigma) (\exists y^\tau) P(x,y) ] => [ (\exists F^{\sigma \to \tau}) (\forall x^\sigma) P(x,Fx) ]

Of course there are no "sets" in this language, only elements of pure finite types. The functional F there is extensional, because E-HA^\omega includes the higher-type extensionality scheme. 

So something additional happens with constructive set theory, beyond the fact the equality on sets is not decidable. My thought has always been that the additional ingredient is the non-effective separation axioms in constructive set theory, but I would appreciate reading any deeper viewpoints on that issue. 

Best,

Carl 

1:  Martin-Löf P. (2009) "100 Years of Zermelo’s Axiom of Choice: What was the Problem with It?" In: Lindström S., Palmgren E., Segerberg K., Stoltenberg-Hansen V. (eds) Logicism, Intuitionism, and Formalism. Synthese Library (Studies In Epistemology. Logic, Methodology, and Philosophy of Science), vol 341.


-- 
Dr. Carl Mummert
Associate Professor of Mathematics
Marshall University
1 John Marshall Drive
Huntington, WV 25755



On 4/29/18, 11:51 AM, "fom-bounces at cs.nyu.edu on behalf of Robert Black" <fom-bounces at cs.nyu.edu on behalf of mongre at gmx.de> wrote:

[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