A functional interpretation for nonstandard arithmetic

作者：van den Berg Benno^*; Briseid Eyvind; Safarik Pavol

来源：Annals of Pure and Applied Logic, 2012, 163(12): 1962-1994.

DOI：10.1016/j.apal.2012.07.003

• Proof theory
• Functional interpretations
• Nonstandard arithmetic

We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to Godel 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 E-HA(omega) and E-PA(omega), strengthening earlier results by Moerdijk and Palmgren, and 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, including some initial results on saturation principles.

• 出版日期2012-12