"A non-standard model of arithmetic"

Abstract:
We will discuss a sheaf model for Heyting arithmetic. The model itself is known for quite a while and was first described in an ad-hoc fashion by I. Moerdijk. We will give a more systematic description of this model, and show that it is in partiular a kind of saturated model. Also, we will axiomatize the class of all infinitary first-order formulae that are true in this model.