Nonstandard proof methods in toposes

TL;DR

This paper identifies conditions under which toposes can replicate nonstandard analysis techniques, enabling their application in new mathematical contexts like toposes of G-sets and Boolean étendues.

Contribution

It establishes the structure needed for elementary toposes to emulate Nelson's Internal Set Theory and shows that toposes with the internal axiom of choice serve as universes of standard objects.

Findings

Toposes satisfying certain structures can emulate nonstandard analysis methods.

Any topos with the internal axiom of choice acts as a universe of standard objects.

Enables proof techniques like transfer, standardisation, and idealisation in new topos environments.

Abstract

We determine sufficient structure for an elementary topos to emulate E. Nelson's Internal Set Theory in its internal language, and show that any topos satisfying the internal axiom of choice occurs as a universe of standard objects and maps. This development allows one to employ the proof methods of nonstandard analysis (transfer, standardisation, and idealisation) in new environments such as toposes of $G$-sets and Boolean \'etendues.