[FOM] Arithmetic categoricity of CZF

[Roger Bishop Jones]

In the message:
http://www.cs.nyu.edu/pipermail/fom/2009-June/013788.html

Peter Aczel wrote:

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

This sounds like magic, to get fewer theorems AND fewer models,
so presumably there is a significant change to the semantics
which secures this effect, and presumably also CZF+EM also
has a unique model of the Dedeking-Peano axioms.

I have long believed that classical well-founded first
order set theories should be construed under a semantics
which excludes non-well-founded sets.

Is there a concise description of the relevant change to the
semantics? (relative to classical first order model theory)

Roger Jones