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

[Albert Ziegler]

Hi Arnon,

>  a) Is  the class of all functions Nat -> {0,1} a set in CZF?

Yes. While CZF doesn't believe in powersets, it's a theorem that for
two sets A and B, their function space A->B is again a set.

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

Yes, all these basic set operations are recognized by CZF, so this is
a function. It is not an isomorphism however:

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

The function is not surjective: The subsets of N which have such a
characteristic function are precisely the detachable subsets, i.e.
those where it can be decided whether a number belongs to them or not
(just apply the characteristic function to the number and check
whether whether you get zero or one).

But in the multicoloured world of constructive mathematics, there is
no reason why every subset of N should behave in such a monochromatic
way: The set of indices for halting Turing machines for example cannot
be proved to be detachable.

If we try to repair the isomorphism, the obvious way out is to include
not only the classical truth values {0, 1} in the codomain of
characteristic functions but all other constructive truth values, sets
where it might not be decidable whether they are 0 or 1.
Set-theoretically speaking, we realize that we should not have taken
{0, 1} but rather P(1).

But CZF doesn't recognize P(1) as a set. So what this isomorphism
argument shows is that "P(N) exists" can be reduced to "P(1) exists".
But as P(1) is not available, this won't convince CZF of the existence
of P(N).

Albert