Overtness is the lattice dual of compactness, just as open and closed subspace, open and proper maps and discrete and Hausdoff spaces are dual notions. Logically, an overt space is one over which unions and existential quantifiers may range, but in traditional topology this is all of them, so the concept is invisible.
We are better able to understand the idea for familiar spaces such as R^{n} and when we use bases such as the collection of balls instead of the lattices of all open subspaces.
Then we find that overtness agrees with locatedness in constructive analysis. In order to prove constructive versions of many theorems of classical functional analysis, we need to assume that some subspace, such as the kernel of a linear map, is located.
There is a "distance" function saying how far a general point is from an overt or located subspace of R^{n}. This satisfies
The second property invites iteration, converging to a limit a, so that
In fact, properties like these are familiar from classical numerical analysis. This means that overtness and locatedness can be understood by mathemeticians who are more comfortable with using metrical ideas than logical ones.
For example, the familiar Newton-Raphson algorithm for finding a zero of a continuously differentiable function gives, at each step, a correction to the current estimate. Under appropriate conditions, this actually provides (an upper bound for) the distance to the nearest zero. It is a simple matter to derive a distance function with all of the above properties from the one that comes from the algorithm.
More generally, any algorithm that yields a point of R^{n} from discrete starting data defines an overt subspace, whilst the defining formula of any overt subspace yields a computable (though in general infeasible) algorithm for the points of a countable net that is dense in the subspace.
Hence overtness is a concept of general topology that exactly captures subspaces of points that are the results of processes of solving equations (as opposed to points that happen to satisfy the equations). A pure mathematician may work with a problem topologically, defining its overt subspace of solutions, and hand the formula over to a computational proof theorist to evaluate the solution.
Overtness is in this sense the demarcation between mathematics and computation.
Dr Walter Dean
Department of Philosophy
University of Warwick
http://go.warwick.ac.uk/whdean