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