Elementary real analysis in the nonstandard universe

Our main subject in this Chapter will be the development of nonstandard real analysis in the frameworks of the foundational scheme “$${\text{WF}}\xrightarrow{*}\left| {\left[ {{\text{in}}{\kern 1pt} {\text{H}}} \right]} \right.$$” of HST (as explained in § 1.2a). Of course, by no means can we hope to prove any new mathematical fact this way: indeed, if Φ is an ∈-sentence then Φwf, the relativization of Φ to WF, is provable in HST if and only if Φ is a theorem of ZFC (Theorem 1.1.14). Yet a broader “external” view brings us new insights into the nature of very common mathematical objects, or rather restores, at the level of full mathematical rigor, mathematical ideas and constructions once successfully employed by the masters of early calculus but then abandoned as too vague to admit rigorous treatment.