On the computational properties of basic mathematical notions

Abstract

We investigate the computational properties of basic mathematical notions pertaining to $\mathbb{R}\to \mathbb{R}$-functions and subsets of $\mathbb{R}$, like finiteness, countability, (absolute) continuity, bounded variation, suprema, and regularity. We work in higher-order computability theory based on Kleene's S1-S9 schemes. We show that the aforementioned italicised properties give rise to two huge and robust classes of computationally equivalent operations, the latter based on well-known theorems from the mainstream mathematics literature. As part of this endeavour, we develop an equivalent $\hat{I}»$-calculus formulation of S1-S9 that accommodates partial objects. We show that the latter are essential to our enterprise via the study of countably based and partial functionals of type $3$.

The lambda calculus introduced in Section 3 of this paper unfortunately suffers from a technical error. The latter was communicated to us in a private communication by John Longley. A corrected version may be found in Section 5 of arXiv:2401.09053. The computability theoretic results in this paper remain unaffected