Foundations for Computable Topology

Foundations for Computable Topology

[Paul Taylor]

       Foundations for Computable Topology
       www.PaulTaylor.EU/ASD/foufct/

This paper is an overview of the whole of the Abstract Stone Duality
research programme.   I was invited to write it for a volume on
Foundations of Mathematics that is more inclined towards philosophy
than technicalities and has contributions from categorists, set
theorists and philosophers.  I advertised this in July, but the
production timescale of this book has slipped somewhat, so I would
still welcome comments.   In particular, I have some questions
below about citations for the history of category theory.

The plan of the paper is as follows:
1. Foundations should be designed FOR mathematics.
2. The formal link between category theory and symbolic logic.
3. Using this as a methodology to design the new theory.
4. Stone duality between topology and algebra over sets
5. Stone duality as a monad, with applications to topology
6. The axiomatic "monadic framework".
7. The subobject classifier and Sierpinski space.
8. Axiomatic development of set theory using the Euclidean principle
    and topology using the Phoa principle.
9. Discrete mathematics using overt discrete spaces,
    arithmetic universes, recursion, description.
10. The "underlying set" axiom, which makes the full subcategory
    of overt discrete spaces into a topos.
11. Scott continuity as an axiom.
12. Beyond local compactness.

The version of the last section as it appeared in July was COMPLETELY
SCRAPPED, and replaced with a discussion of "equideductive logic",
about which I talked at meetings in Sussex in September and Padova
in October.  Even in the present version, I still intend to replace
the last few pages with a "conclusion".

Briefly, equideductive logic is the (surprisingly interesting) logic
of regular monos in a CCC with all finite limits.   It is exactly
what is required to perform Dana Scott's "equilogical space"
construction, but without using the set theoretic interpretation
based on the set of points of the basic spaces.   I have done further
work on this, but I am nowhere near being ready to advertise it.

This paper does not discuss computation,  but Andrej Bauer did some
interesting programming during the summer:
math.andrej.com/2008/08/24/efficient-computation-with-dedekind-reals/

SOME HOSTORICAL QUESTIONS

Recall that the purpose of my paper is to give a general overview of
the philosophy and motivations of ASD, along with a statement of all
of the axioms for reference.   I am therefore looking for citations
that are also of a survey, historical or philosophical flavour,
rather than the original technical source.   The numbers refer to
the subsections or paragraphs -- the paper is written in a narrative
style, without Definition--Lemma--Theorem--Proof.   The non-bracketed
text is quoted from my paper.

2.6 [In a discussion of the relationship between category theory and
symbolic logic.] Systems such as linear logic that do not obey all of
the
structural rules correspond to different categorical structures.
These might, for example, be \emph{tensor} products~($\otimes$), which
categorists understood long before they did predicate logic.

3.7 [In a critique of point--set topology.] Sheaves in algebraic
geometry were based on open sets and not points

3.8 These books [on point--set topology] ... make little attempt to
explore the full extent of even the world that is measured out by
their own co-ordinate system.  This was only begun when the analogy
with the $\exists\land$-fragment of logic was recognised.

5.1 For this, we need a way of formulating (potentially infinitary)
algebraic theories that works over an arbitrary category $\S$, and not
just over the category of sets.  Such an account is provided by the
categorical notion of \emph{monad}.   [Has anyone ever tried to
write a textbook that covers the material of Modern or Universal
Algebra using monads?]

6.12 The problem of finding splittings is actually not a new one: it
was well known in homological algebra, which provided Jon Beck's
original inspiration. [Can you give me a simple example of the use
of splittings in homological algebra, and the difficulty in finding
them?]

9.1 Finite limits and stable effective quotients of equivalence
relations were studied in category theory long before it considered
logic, because categories of finitary algebras inherit them from sets.

9.12 For terms and parameters of these types, Scott continuity is a
\emph{theorem}, essentially the one of Henry Rice and Norman Shapiro.

Paul Taylor
pt09 @ PaulTaylor.EU
www.PaulTaylor.EU/ASD/foufct