Personal tools
You are here: Home Events Abstract Archives 2001 Non-standard models of intuitionistic and classical theories

Non-standard models of intuitionistic and classical theories

Carsten Butz Heriot-Watt University 4pm, Wednesday 18 April 2001 Room 2511, JCMB, King's Buildings

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.

Document Actions