Topology via Logic

( Topology Series )

Steve Vickers, School of Computer Science

Date and time: Wednesday 14th January 2004 at 16:30
Location: 217, School of Computer Science

This is the first talk in Steve Vickers' Topology via Logic series:

I am giving a series of talks this term on topology from a computer science perspective. It will in many ways follow my book "Topology via Logic" (CUP 1989), but will also go beyond that in bringing out the deep relationship with constructive logic. My lectures will be new, and in fact part of the aim is to put together the shape of a constructive 2^nd edition of Topology via Logic.

Copies of slides are available.

Outline:

1. via Logic: In my book, "via Logic" referred to the way it presents topologies as Lindenbaum algebras for theories in a particular non-classical logic, the so called geometric logic. This lies behind an alternative approach to topology known as locale theory, which has been used in the semantics of programming languages - notably in Abramsky's thesis.
2. Observability: In my book I motivate the use of geometric logic by an informal discussion of how certain logical connective have observational content (this is also present in the work of Smyth and Abramsky). Then the basic deal in semantics is that a domain, with its Scott topology, embodies a logical theory of how one can observe some type of program by watching it run (without access to the source code).
3. Going constructive: The book is entirely classical in its mathematics. However, since it was written I have come to understand much better the key role of constructive mathematics in topology and have exploited it in my papers such as "Topical categories of domains". This is what I want to explain in the lectures.
4. Better constructive topology: One aspect of this is that if you are already committed to constructivism (maybe in order to take better account of computational issues), then the localic approach is known to give better results in constructive topology than topology itself.
5. Continuity for free. But there are deeper reasons topological reasons for being constructive. Associated with the geometric logic, there is a "geometric mathematics". It is constructive, and also has an intrinsic continuity. If you adhere to the constructive constraints of geometric reasoning then you do not have to give explicit continuity proofs - continuity is automatic. In effect, the usual continuity proofs in classical reasoning are bureaucratic certifications that you haven't transgressed the geometric constraints. So there are quite practical reasons for accepting those constraints.
6. Toposes A major spinoff is that the same approach adapts quite naturally to a generalization of topological space, namely toposes. This aspect of toposes is normally concealed, but it is fundamental to their importance. Roughly speaking, from this point of view a (Grothendieck) topos is a topological space for which there are "not enough opens" and instead the topological structure has to be defined through what are known as its sheaves.