Abstract

Using infinitary logic we will introduce an intuitionistic notion of saturated models and study such models of Heyting arithmetic. Instances of our notion of saturated models have been used before: With the help of such models Moerdijk and Palmgren proved a strong conservativity result for Heyting arithmetic (we will recapitulate this), and saturated models play a central role in Palmgren's development of intuitionistic non-standard analysis. Our definition of saturated models is closely related to a filter construction on categories introduced by A. Pitts, and also relates to the topos(es) of types introduced by M. Makkai, and those connection will be made clear.

We will also demonstrate how our theory leads to a possibly new approach to classical non-standard analysis as invented by A. Robinson.