Week 3, 14 October 2014 (16:00-18:00 Watson R17/18)

Paul Taylor

Title: Overt Subspaces of Rn


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 Rn 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 Rn. This satisfies

  • d(x) < r iff for some r' s.t. d(x) < r' < r
  • d(x) < r ==> for all ε > 0 , there is some x' s.t. d(x') < ε and d(x,x') < r
  • d(x) < r & d(x,y) < s ==> d(y) < r+s

The second property invites iteration, converging to a limit a, so that

d(x) < r iff for some a s.t. d(x,a) < r & d(a) = 0

where d(a) = 0 means for all r>0 s.t. d(a) < r , and we call such a an accumulation point.

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 Rn 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.

About the seminar

The Midlands Logic Seminar was founded in 2011 and aims to cover all areas of mathematical logic, as well as related areas of theoretical computer science and philosophy of mathematics.

Study group

Our topic for Term 1 of 2014-2015 is the use of induction and heuristics in mathematical problem solving. We will be working through George Polya's book Induction and Analogy in Mathematics .


All meetings for Term 1 2014-15 will be Tuesday from 16:00-18:00 (study group 16:00-17:00, research talks 17:00-18:00) in room 310 of Watson Building (TBC) on the campus of the University of Birmingham.
  • campus map
  • google maps
    To get to campus, take the train from Birmingham New Street to the University stop (7 minutes).


    Dr Richard Kaye
    School of Mathematics
    University of Birmingham


    Dr Walter Dean
    Department of Philosophy
    University of Warwick