Dispensing with the continuum

Abstract

We present a constructive system of nonstandard analysis, called elementary recursive nonstandard analysis (ERNA), as a viable foundation for the mathematics that is used in the empirical sciences; the viability is demonstrated by showing that a version of the standard existence theorem for first-order ordinary differential equations is provable in ERNA. We demonstrate the constructive character of ERNA by showing that it has a finitary consistency proof. Through the consistency proof one can make the observation that ERNA has models in which every element is a (possibly nonstandard) rational number; hence properties special to the continuum are not used in ERNA. Also, we will show how the consistency proof leads to the construction of finite models in the standard rationals. Then we give an isomorphism theorem stating that the interpretation of any finite set of ERNA-terms can be mapped, isomorphically, onto a finite set of standard rationals. Additionally, we discuss to what extent such isomorphisms are constructive and how the isomorphism theorem lends further support to the thesis that the continuum is dispensable in the mathematics that is used in the empirical Sciences. © 1997 Academic Press.