"A realizability model for Nonstandard Arithmetic"

Jaap van Oosten

It is well known that even in intuitionistic set theory, a proper 
elementary extension of N as a model of first-order arithmetic, 
forces this first-order arithmetic to be classical.
The situation is even worse in the world of Kleene realizability: 
as Charles McCarty showed in the 1980's, there can be no nonstandard 
model of arithmetic at all. 
In fact, a recent sharpening by Benno van den Berg and me is, 
that in the effective topos there is exactly one model of 
I\Sigma _1 (arithmetic with only induction for \Sigma _1-formulas):
the standard natural numbers object.
However, there is an interesting subtopos of the effective topos, 
for a local operator first exhibited by A. Pitts, which is 
non-Boolean yet has classical first-order arithmetic. 
In this topos, we can mimick an old construction by Skolem to 
produce an elementary extension of the standard model of arithmetic.