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

[Peter Aczel]

Perhaps the following facts may help clarify things.

1) There is an axiom system, CZF, for Constructive Set Theory,
that is formulated in the language of ZF, but uses intuitionistic
logic rather than classical logic.

2) If the law of excluded middle is added to CZF, to get CZF+EM,
so that the logic is classical, then CZF+EM has the same theorems
as ZF.

3) In CZF there is a unique model, up to isomorphism, (Nat, ...),
of the Dedekind-Peano axioms for the set Nat of natural numbers.

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.

6) There is an axiom system T such that, in CZF there is a unique
model, up to isomorphism, (Real, ...), of T.  T is an axiom system
for the pseudo-ordered field of located Dedekind real numbers.

7) In CZF Real is an uncountable set.

Peter Aczel
Manchester University
email: petera at cs.man.ac.uk