[FOM] More on CZF

[Peter Aczel]

> Where can we read more about CZF?

You might want to look at my publications web page for more on CZF, etc.

http://www.cs.man.ac.uk/~petera/papers.html

See also Michael Rathjen's web page

http://www.maths.leeds.ac.uk/~rathjen/preprints.html

Best wishes,

Peter Aczel

>
> --- 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
>>
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>