Transfer principles in nonstandard intuitionistic arithmetic

Archive for Mathematical Logic 41 (6):581-602 (2002)
  Copy   BIBTEX

Abstract

Using a slight generalization, due to Palmgren, of sheaf semantics, we present a term-model construction that assigns a model to any first-order intuitionistic theory. A modification of this construction then assigns a nonstandard model to any theory of arithmetic, enabling us to reproduce conservation results of Moerdijk and Palmgren for nonstandard Heyting arithmetic. Internalizing the construction allows us to strengthen these results with additional transfer rules; we then show that even trivial transfer axioms or minor strengthenings of these rules destroy conservativity over HA. The analysis also shows that nonstandard HA has neither the disjunction property nor the explicit definability property. Finally, careful attention to the complexity of our definitions allows us to show that a certain weak fragment of intuitionistic nonstandard arithmetic is conservative over primitive recursive arithmetic.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Models of intuitionistic TT and N.Daniel Dzierzgowski - 1995 - Journal of Symbolic Logic 60 (2):640-653.
Nonstandard arithmetic and reverse mathematics.H. Jerome Keisler - 2006 - Bulletin of Symbolic Logic 12 (1):100-125.
Developments in constructive nonstandard analysis.Erik Palmgren - 1998 - Bulletin of Symbolic Logic 4 (3):233-272.
Inconsistent nonstandard arithmetic.Chris Mortensen - 1987 - Journal of Symbolic Logic 52 (2):512-518.
Classical arithmetic as part of intuitionistic arithmetic.Michael Potter - 1998 - Grazer Philosophische Studien 55 (1):127-41.
On certain types and models for arithmetic.Andreas Blass - 1974 - Journal of Symbolic Logic 39 (1):151-162.
On the complexity of models of arithmetic.Kenneth McAloon - 1982 - Journal of Symbolic Logic 47 (2):403-415.

Analytics

Added to PP
2009-01-28

Downloads
111 (#156,334)

6 months
5 (#638,139)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Jeremy Avigad
Carnegie Mellon University

Citations of this work

A functional interpretation for nonstandard arithmetic.Benno van den Berg, Eyvind Briseid & Pavol Safarik - 2012 - Annals of Pure and Applied Logic 163 (12):1962-1994.
Saturated models of universal theories.Jeremy Avigad - 2002 - Annals of Pure and Applied Logic 118 (3):219-234.
Forcing in proof theory.Jeremy Avigad - 2004 - Bulletin of Symbolic Logic 10 (3):305-333.
Saturated models of intuitionistic theories.Carsten Butz - 2004 - Annals of Pure and Applied Logic 129 (1-3):245-275.

View all 7 citations / Add more citations

References found in this work

Sheaves and Logic.M. P. Fourman, D. S. Scott & C. J. Mulvey - 1983 - Journal of Symbolic Logic 48 (4):1201-1203.
Interpreting classical theories in constructive ones.Jeremy Avigad - 2000 - Journal of Symbolic Logic 65 (4):1785-1812.
A model for intuitionistic non-standard arithmetic.Ieke Moerdijk - 1995 - Annals of Pure and Applied Logic 73 (1):37-51.
Developments in constructive nonstandard analysis.Erik Palmgren - 1998 - Bulletin of Symbolic Logic 4 (3):233-272.
Minimal models of Heyting arithmetic.Ieke Moerdijk & Erik Palmgren - 1997 - Journal of Symbolic Logic 62 (4):1448-1460.

View all 12 references / Add more references