Related Work

Often [• ••] the nonstandard definition of a concept is simpler than the standard definition (both intuitively simpler and simpler in a technical sense, such as quantifiers over lower types or fewer alternations of quantifiers). As a result, nonstandard analysis sometimes makes it easier to find proofs. [4, p. 37]

In what follows, we rely on [6] as an up-to-date comparative survey on systems which offer automated proof abilities related to real analysis. Some of the formalizations supported by such systems characterize real numbers axiomatically, as a given set with specific operations and properties; others construct real numbers either from rational Cauchy sequences or as Dedekind cuts. Nonstandard analysis is available in ACL2(r) and in Isabelle/HOL (see [26, 27], respectively): both achievements are reminiscent of [2, 3].

The semi-automated theorem prover ACL2, which ACL2(r) potentiates, offers limited support to quantifier handling (cf. [27, pp. 323-324]); in order to circumvent that difficulty, ACL2(r) focuses on the extension 1R of the reals. With hyperreal numbers, in fact, the quantifier alternation V e > 0 3 8 > 0... which affects the usual formulas about limits becomes unnecessary, hence the proofs benefit from a higher degree of automation. The formalism of ACL2(r) is based on an axiomatization of *R as an autonomous domain.

The Isabelle/HOL-mechanization of real analysis, on the other hand, introduces the standard, along with the nonstandard, definition of each concept; thereby, ‘users will have the freedom either to stick with classical (standard) techniques, use nonstandard ones, or a combination of both’ [26, p. 161]. ‘Our first task’, the author notes, ‘each time we introduce a new concept from analysis, is to prove that the two definitions are equivalent’ [26, p. 150]. Thus, albeit implicitly, the transfer principle plays a central role. It is ‘neither an axiom nor a theorem, but a meta-theorem, since it applies to theorem statements’ and, as such, ‘it is not directly proved in Isabelle/HOL’ [6]; nevertheless, since this principle informs the general pattern followed by all the equivalence proofs, the ultrapower construction of the hyperreals presupposed that a proof of Zorn’s lemma and a theory of filters and ultrafilters were developed for Isabelle/HOL (cf. [26, p. 145]).

As an eventual reward of the exploration discussed in this paper, we hope to get Ref-based, nonstandard proofs of theorems of real analysis and to check by means of Ref many of the results presented in Martin Davis’s chapter on hyperreal numbers [14, Sects. 2.3-2.8]. However, a formal remake of real analysis along unconventional lines is only an incidental issue here. As discussed at the beginning, we rather feel confronted with a proof-engineering issue—akin to metamathematical extensibility—which our proof assistant could tackle well because a proof of the relevant meta-theorem can be set up with relative ease in a full-fledged set theory.

After all, the guidelines for a Ref-based development of analysis which J. T. Schwartz sketched in [35, Chap. 5] stick to the tradition; the use of nonstandard methods can lead to much simpler and more elegant proofs than the classical ones, but one can contend that it calls for an extra amount of work spent on preliminary constructions, which may be out of scale with a proof of Rolle’s theorem (to cite a result of analysis proper).

For a large-scale endeavor, this additional work is justified by considerations such as the following:

Not only does nonstandard analysis provide a rigorous treatment of infinitesimals in the area of mathematics where they were originally used, it also gives elegant approaches to some ideas that developed later.

[4, p. 37]

< Prev   CONTENTS   Source   Next >