Paper Info
Title
A sheaf-theoretic foundation for nonstandard analysis
Abstract
A new foundation for constructive nonstandard analysis is presented. It is based on an extension of a sheaf-theoretic model of nonstandard arithmetic due to I. Moerdijk. The model consists of representable sheaves over a site of filter bases. Nonstandard characterisations of various notions from analysis are obtained: modes of convergence, uniform continuity and differentiability, and some topological notions. We also obtain some additional results about the model. As in the classical case, the order type of the nonstandard natural numbers is a dense set of copies of the integers. Every standard set has a hyperfinite enumeration of its standard elements in the model. All arguments are carried out within a constructive and predicative metatheory: Martin-Löf's type theory.
Year
DOI
Venue
1997
10.1016/S0168-0072(96)00041-3
Annals of Pure and Applied Logic
Keywords
DocType
Volume
nonstandard analysis,type theory
Journal
85
Issue
ISSN
Citations 
1
0168-0072
5
PageRank 
References 
Authors
1.36
4
1
Name
Order
Citations
PageRank
Erik Palmgren123343.17