[FOM] Pow(Nat) in CZF

[Peter Aczel]

>  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

The proof that your suggested `classical isomorphism' is surjective
makes obvious use of the law of excluded middle.  In fact your function
gives a bijection between the set Nat -> {0,1} and the class D(Nat) of
decidable subsets of Nat, showing, using Replacement, that D(Nat) is
a set.

Best wishes,

Peter Aczel

Peter