A functional interpretation for nonstandard arithmetic

B. van den Berg; E. Briseid; P. Safarik

doi:10.1016/j.apal.2012.07.003

A functional interpretation for nonstandard arithmetic

B. van den Berg, E. Briseid, P. Safarik

extern

Research output: Contribution to journal › Article › Academic › peer-review

Abstract

We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to Gödel 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ω and E-PAω, 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.

Original language	English
Pages (from-to)	1962-1994
Number of pages	33
Journal	Annals of Pure and Applied Logic
Volume	163
Issue number	12
DOIs	https://doi.org/10.1016/j.apal.2012.07.003
Publication status	Published - 2012

Access to Document

10.1016/j.apal.2012.07.003

Embargoed Document

1091-main[1]
Final published version, 401 KB
Embargo ends: 1/01/50

Cite this

@article{e0c4896908e2460b9f5035744791a5fc,

title = "A functional interpretation for nonstandard arithmetic",

abstract = "We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to G{\"o}del 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ω and E-PAω, 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.",

author = "{van den Berg}, B. and E. Briseid and P. Safarik",

year = "2012",

doi = "10.1016/j.apal.2012.07.003",

language = "English",

volume = "163",

pages = "1962--1994",

journal = "Annals of Pure and Applied Logic",

issn = "0168-0072",

publisher = "Elsevier",

number = "12",

}

TY - JOUR

T1 - A functional interpretation for nonstandard arithmetic

AU - van den Berg, B.

AU - Briseid, E.

AU - Safarik, P.

PY - 2012

Y1 - 2012

N2 - We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to Gödel 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ω and E-PAω, 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.

AB - We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to Gödel 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ω and E-PAω, 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.

U2 - 10.1016/j.apal.2012.07.003

DO - 10.1016/j.apal.2012.07.003

M3 - Article

SN - 0168-0072

VL - 163

SP - 1962

EP - 1994

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

IS - 12

ER -

A functional interpretation for nonstandard arithmetic

Abstract

Access to Document

Embargoed Document

Fingerprint

Cite this