A functional interpretation for nonstandard arithmetic

2011/09/14 by Benno van den Berg, Berg, Benno van den, Eyvind Briseid +3 · 1 citation
Mathematics · #03F10 #03F30 #03F50 #11U10 #26E35 #FOS: Mathematics #Logic (math.LO) #math.LO #msc:03F10 #msc:03F30 #msc:03F50 #msc:11U10 #msc:26E35

paper · pdf · doi:10.48550/arxiv.1109.3103

arxiv created 2012/07/19 · arxiv updated 2012/07/20

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.

Cited by

• The Uniform Functional Interpretation with Informative Types

Related

• A note on non-classical Nonstandard Arithmetic
• The strength of countable saturation
• Reverse Mathematics and parameter-free Transfer
• The Gandy-Hyland functional and a hitherto unknown computational aspect of Nonstandard Analysis
• Non-standard Nonstandard Analysis and the computational content of standard mathematics