Sheaf Models for Intuitionistic Non-Standard Arithmetic
Maaike Annebeth Zwart
Abstract:
The aim of this thesis is twofold. Firstly, to find and analyse models for non-standard natural arithmetic in a category of sheaves on a site. Secondly, to give an introduction in this area of research.
In the introduction we take the reader from the basics of category theory to sheaves and sheaf semantics. We purely focus on the category theory needed for sheaf models of non-standard arithmetic. To keep the introduction as brief as possible while still serving its purpose, we give numerous examples but refer to the standard literature for proofs.
In the remainder of the thesis, we present two sheaf models for intuitionistic non-standard arithmetic. Our sheaf models are inspired by the model I. Moerdijk describes in A model for intuitionistic non-standard arithmetic.
The first model we construct is a sheaf in the category of sheaves over a very elementary site. The category of this site is a poset of the infinite subsets of the natural numbers. Apart from the Peano axioms, our sheaf models the non-standard principles overspill, underspill, transfer, idealisation and realisation. Many of our results depend on a classical meta-theory. Moerdijkâ€™s proofs are fully constructive, which is why we improve our site for our second model.
For the second model, we use a site with more structure. In the category of sheaves on this second site, we find a non-standard model that much resembles our first model. We get the same results for this model and are able to prove some of the results that previously needed classical meta-theory, constructively. However, there remain principles of which we can only show validity in our model using classical logic in the meta-theory.
Lastly, we try to construct a non-standard model using a categorical version of the ultrafilter construction on the natural numbers object of the category of sheaves on our first site. This yields a sheaf which has both the natural numbers object and our first model as subsheaves.