Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis

John Cowles
(University of Wyoming)
Ruben Gamboa
(University of Wyoming)

ACL2(r) is a variant of ACL2 that supports the irrational real and complex numbers. Its logical foundation is based on internal set theory (IST), an axiomatic formalization of non-standard analysis (NSA). Familiar ideas from analysis, such as continuity, differentiability, and integrability, are defined quite differently in NSA–some would argue the NSA definitions are more intuitive. In previous work, we have adopted the NSA definitions in ACL2(r), and simply taken as granted that these are equivalent to the traditional analysis notions, e.g., to the familiar epsilon-delta definitions. However, we argue in this paper that there are circumstances when the more traditional definitions are advantageous in the setting of ACL2(r), precisely because the traditional notions are classical, so they are unencumbered by IST limitations on inference rules such as induction or the use of pseudo-lambda terms in functional instantiation. To address this concern, we describe a formal proof in ACL2(r) of the equivalence of the traditional and non-standards definitions of these notions.

In Freek Verbeek and Julien Schmaltz: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014), Vienna, Austria, 12-13th July 2014, Electronic Proceedings in Theoretical Computer Science 152, pp. 89–100.
Published: 4th June 2014.

ArXived at: http://dx.doi.org/10.4204/EPTCS.152.8 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org