[FOM] From the moderator (was "Constructivism, Geometry, and Powerset") (Martin Davis)

[Arnon Avron]

Dear Peter

> 4) There is no proof in CZF that the powerclass Pow(Nat) of all
> subsets of Nat is a set.
> 
> 5) In CZF the class of all functions Nat -> Nat is a set.

Th`is issue is only remotedly related to my main concern in
my latest postings (the relations between R and the 
geometric line). Moreover, with my classically-oriented
mind, I find Nat -> Nat as no less problematic 
then P(N), and the fact that constructivists see things
differently would not change this. However, your
clarifications makes me curious to know (note that
I am NOT trying to argue, and I am not going to argue):

 a) Is  the class of all functions Nat -> {0,1} a set in CZF?
 b) If so, is the usual classical isomorphism 
    between Nat -> {0,1} and P(N):
        \lambda f:Nat -> {0,1}.{x\in Nat|f(x)=1} 
    accepted as a legitimate function in CZF?
 c) If the answer to b) is "no", what is unconstructive
    about that isomorphism? If the answer is "yes",
    how come P(N) is not available in CZF?
 
Arnon