A model for intuitionistic non-standard arithmetic (Q1891250)

Let \(F\) be the category of filters on subsets of \(\mathbb{N}^k\), where \(\mathbb{N}\) is the set of natural numbers and \(k\geq 0\). \(F\) is equipped with a Grothendieck topology, and the sheaves of \(F\) form a topos. The sheaf \(N\), corresponding to the set \(\mathbb{N}\) and its trivial filter \(\{\mathbb{N}\}\), is interpreted as a model for the language of first-order arithmetic. Semantics for \(N\) is defined via Kripke-Joyal forcing relation. It is shown that under this interpretation \(N\) is a model of true arithmetic. Proofs are constructive and can be formalized within higher-order Heyting arithmetic. Variations of the construction, using arithmetically definable sets, and filters on the Baire space, are also given.