Tripos models of Internal Set Theory

Abstract

This thesis provides a framework to make sense of models of E. Nelson’s Internal Set Theory (and hence of nonstandard analysis) in elementary toposes by exploiting the technology of tripos theory and Lawvere’s hyperdoctrines. A new doctrinal account of nonstandard phenomena is described, which avoids a few key restrictions in Nelson’s approach: chiefly, the dependence on Set Theory (which is done by replacing a model of set theory with a topos as the starting point) and reliance on an internally defined notion of standard element. From the new perspective, validity of the schemes of Idealisation, Standardisation, and Transfer correspond to the existence of certain relationships between hyperdoctrines, leading to the new notion of a tripos model of IST. After discussing the properties of such models that make them a suitable abstraction of classic IST we explore situations in which such structures arise, leading to two distinct main classes of models: what we refer to as Nelson models, which are those for which there is a well-behaved `predicate of standard elements’ (providing thus a close approximation of classic IST valid for toposes), and models obtained by elaborating on the work started by A. Kock and C. J. Mikkelsen on the categorification of Transfer. We then elaborate upon one particular kind of model of each type: the ultrapower models, which are Nelson models obtained from a choice of adequate ultrafilter and that mirror the constructions of classical Robinson nonstandard analysis, and the localic models for Transfer and Standardisation, which are obtained from any given open surjection of locales (e.g universal covers of topological spaces) via the Kock-Mikkelsen construction at the level of sheaf toposes.