A Constructive Approach to Nonstandard Analysis

Erik Palmgren, Annals of Pure and Applied Logic 73(1995), 297 - 325.

Abstract. In this paper we introduce a constructive theory of nonstandard arithmetic in higher types. The theory is intended as a framework for developing elementary nonstandard analysis constructively. More specifically, the theory introduced is a conservative extension of $HA^+omega + AC$. A predicate for distinguishing standard objects is added as in Nelson's internal set theory. Weak transfer and idealisation principles are proved from the axioms. Finally, the use of the theory is illustrated by extending Bishop's constructive analysis with infinitesimals.

Back to the list of publications.

Erik Palmgren, March 9, 1999.