A constructive approach to nonstandard analysis (Q1892939)

The author introduces a constructive theory that may be useful in developing some of the areas of elementary nonstandard analysis. The theory is a conservative extension of \(\mathbf {HA}^\omega+ \mathbf {AC}\). The author adjoins a predicate, much as is done in Nelson's internal set theory, that distinguishes standard objects. A weak transfer and an idealisation principle are then proved from his axioms. The author illustrates the use of this approach by establishing some of the elementary nonstandard statements relating the hyperreals, infinitesimals, and the usual concepts one associates with elementary real analysis. Of course, this approach is weaker than the customary Robinson methods.