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

TL;DR

This paper formalizes and proves the equivalence between traditional epsilon-delta and non-standard analysis definitions of core concepts in real analysis within the ACL2(r) theorem prover, highlighting when traditional definitions are advantageous.

Contribution

It provides a formal proof of the equivalence between traditional and NSA definitions in ACL2(r), clarifying their relationship and practical use cases.

Findings

Formal proof of equivalence in ACL2(r)

Traditional definitions can be more advantageous in certain contexts

NSA and classical definitions are provably equivalent in ACL2(r)

Abstract

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.