A functional interpretation for nonstandard arithmetic

TL;DR

This paper develops constructive and classical nonstandard arithmetic systems and demonstrates how functional interpretations can translate proofs into standard systems, establishing conservativity and enabling term extraction.

Contribution

It introduces new nonstandard arithmetic systems and adapts functional interpretations to show their conservativity over standard arithmetic, extending prior results.

Findings

Nonstandard systems are conservative extensions of standard arithmetic.

Functional interpretations can be used to rewrite proofs into standard systems.

Initial results on saturation principles and future research directions.

Abstract

We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to Goedel and Shoenfield can be used to rewrite proofs performed in these systems into standard ones. These functional interpretations show in particular that our nonstandard systems are conservative extensions of extensional Heyting and Peano arithmetic in all finite types, strengthening earlier results by Moerdijk, Palmgren, Avigad and Helzner. We will also indicate how our rewriting algorithm can be used for term extraction purposes. To conclude the paper, we will point out some open problems and directions for future research and mention some initial results on saturation principles.