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

[steve newberry]

Where can we read more about CZF?

--- On Wed, 6/3/09, Peter Aczel <petera at cs.man.ac.uk> wrote:

> From: Peter Aczel <petera at cs.man.ac.uk>
> Subject: Re: [FOM] From the moderator (was "Constructivism, Geometry, and Powerset")  (Martin Davis)
> To: fom at cs.nyu.edu
> Date: Wednesday, June 3, 2009, 11:48 PM
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>