Nonstandard functional interpretations and categorical models

Abstract

Recently, van den Berg, Briseid and Safarik introduced nonstandard Dialectica, a functional interpretation that is capable of eliminating instances of familiar principles of nonstandard arithmetic - including overspill, underspill, and generalisations to higher types - from proofs. We show that, under few metatheoretical assumptions, the properties of this interpretation are mirrored by first order logic in a constructive sheaf model of nonstandard arithmetic due to Moerdijk, later developed by Palmgren. In doing so, we also draw some new connections between nonstandard principles, and principles that are rejected by strict constructivism. The categorical analysis suggests that one can obtain nonstandard Dialectica from a variant of the Diller-Nahm interpretion with two different kinds of quantifiers (with and without computational meaning), similar to Hernest’s light Dialectica interpretation, by weakening the computational content of the existential quantifiers - a process we call herbrandisation. As a byproduct of herbrandisation, disjunction is deprived of its constructive content. Finally, we point out some open problems and directions for future research, concerning, in particular, the relation of the sheaf models to certain realisability topos models.