Overt Subspaces of Rⁿ

Abstract

We aim in this paper to give an explanation of the notion of an overt subspace that is suitable for the general mathematician. It is, we claim, a topological idea, and our main theorem is a characterisation of these subspaces in locally compact metric spaces such as Rⁿ. In proving this, we shall only assume such knowledge of metric and topological spaces as may be found in any undergraduate course on those topics.

This concept has arisen in several different constructive formulations of topology and analysis: the reason why it is unfamiliar is that it dissolves into nothing when reduced to classical point–set topology. Its significance comes from the unification of these disciplines with the theory of computation, but again the ideas from computability and logic that we shall need may also be found in introductory courses.

We want to convey the importance of overtness across classical, numerical, constructive and computable mathematics, so we shall write our technical development in traditional notation. We give a brief survey of the many different roots of this idea, but it will not be necessary to understand all or any of the heterodox systems or their notation.

In fact, the main prerequisite will be a willingness to take mathematical ideas au naturel and not try to shoe-horn them into a classical setting.

Download the paper

PDF,  

Version of 22 March 2017.