Abstract Stone Duality - introduction/survey papers

Abstract Stone Duality - introduction/survey papers

[Paul Taylor]

People have been asking me for several years to write "introductions"
to ASD, or to "write down all the axioms together".  This was not
possible while the core theory for locally compact spaces was still
being investigated,  but that process has essentially come to an end.

There are now FOUR introduction/survey papers, aimed at different
audiences, and all available from   www.PaulTaylor.EU/ASD

(lamcra)   "A Lambda Calculus for Real Analysis"
     suitable for a general mathematical audience

(intawi)   "Interval Analysis Without Intervals"
     aimed at programmers of "exact real arithmetic" but not finished

(dedras)   "The Dedekind Reals in Abstract Stone Duality"
     (with Andrej Bauer) suitable for theoretical computer scientists

(foufct)   "Foundations for Computable Topology"

I was invited to write this last paper for a volume on Foundations
of Mathematics that is more inclined towards philosophy than
technicalities and has contributions from categorists, set theorists
and philosophers.

My paper therefore begins with a discussion of the methodology behind
ASD, and in particular the thesis that foundations can be devised
FOR mathematics (rather than vice versa)  by encapsulating headline
theorems as universal properties and translating these into systems
of introduction/elimination/beta/eta rules for new logical connectives.

ASD abstracts Stone duality between algebra and topology by saying
that the carriers of the algebras belong to the dual category of
spaces, and formalises this as a monad.   The topological meaning
of Beck's characterisation of monadic adjunctions is that (certain)
equalisers exist and carry the subspace topology in a canonical way.
Several examples of this are given, in particular related to compactness
of the real closed interval.   Then the lambda calculus associated
with the monad is described.

The key object is the Sierpinski space Sigma.  The Euclidean and
Phoa principles are deduced from the property of classifying all,
open or closed subsets.  (A proof is included that Sierpinski
classifies closed sublocales.)   Conversely, the monadic and
Euclidean principles make Sigma a dominance.   Discrete, Hausdorff,
compact and overt spaces are discussed.

Set theory (ie the theory of discrete spaces) is used as a comparative
case.  Although most of the details of other arguments are only
sketched,  this paper includes the whole of the proof of the
characterisation of elementary toposes using the ideas of ASD,
without any mention of subobjects.

Sketches of other parts of the theory are also given.  The paper
tries to tell the whole story of the development of ASD, from a
foundational and empirical point of view,   It is therefore of
necessity a "broad brush" approach, as the material would easily
fill a book.   This paper is also meant to be complementary to
the others listed above,  so it says very little about the
applications to elementary real analysis.

It also says very little about the computational interpretation
of ASD, but, at least as far as the real numbers are concerned,
you can expect to hear more from Andrej and me on this subject
in the future.

If you would like to comment on "Foundations for Computable Topology",
please do so before the end of July.

Paul Taylor
www.PaulTaylor.EU/ASD/foufct