[FOM] Arithmetic categoricity of CZF

[Roger Bishop Jones]

On Sunday 21 June 2009 07:12:02 Roger Bishop Jones wrote:
>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.
>
>{RBJ]
>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.

Its clear to me now, after further input from Peter,
that I misunderstood what he meant in (3).
He meant (I now believe) that the categoricity of the
Dedkind-Peano axioms, insofar as it can be stated in CZF,
is a theorem of CZF.

I don't now believe that he meant that if the natural
numbers are defined in CZF using (something like)
the Dedekind-Peano axioms (or any other way) then
there are no models of this theory
with non-standard arithmetic.

I understand that there is no special semantics for
CZF and note that the the combination of the semantics
of first order logic (relative to which FOL is complete)
and Godel's first incompleteness result, entail that
there can be no definition of the natural numbers
in CZF which excludes non-standard models of arithemetic.

Roger Jones