Nonstandard functional interpretations and categorical models

Recently, the second author, Briseid, and Safarik introduced nonstandard Dialectica, a functional interpretation capable of eliminating instances of familiar principles of nonstandard arithmetic—including overspill, underspill, and generalizations to higher types—from proofs. We show that 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, and draw some new connections between nonstandard principles and principles that are rejected by strict constructivism. Furthermore, we introduce a variant of the Diller–Nahm interpretation with two different kinds of quantifiers, similar to Hernest’s light Dialectica interpretation, and show that one can obtain nonstandard Dialectica by weakening the computational content of the existential quantifiers—a process called herbrandization. We also define a constructive sheaf model mirroring this new functional interpretation, and show that the process of herbrandization has a clear meaning in terms of these sheaf models.