The Dedekind reals in abstract Stone duality.

Abstract Stone Duality (ASD) is a direct axiomatisation of general topology, in contrast to the traditional and all other contemporary approaches, which rely on a prior notion of discrete set, type or object of a topos. ASD reconciles mathematical and computational viewpoints, providing an inherently computable calculus that does not sacrifice key properties of real analysis such as compactness of the closed interval. Previous theories of recursive analysis failed to do this because they were based on points; ASD succeeds because, like locale theory and formal topology, it is founded on the algebra of open subspaces. ASD is presented as a lambda calculus, of which we provide a self-contained summary, as the foundational background has been investigated in earlier work. The core of the paper constructs the real line using two-sided Dedekind cuts. We show that the closed interval is compact and overt, where these concepts are defined using quantifiers. Further topics, such as the Intermediate Value Theorem, are presented in a separate paper that builds on this one. The interval domain plays an important foundational role. However, we see intervals as generalised Dedekind cuts, which underly the construction of the real line, not as sets or pairs of real numbers. We make a thorough study of arithmetic, in which our operations are more complicated than Moore's, because we work constructively, and we also consider back-to-front (Kaucher) intervals. Finally, we compare ASD with other systems of constructive and computable topology and analysis. 1. Introduction 757 2. Cuts and intervals 762 3. Topology as lambda calculus 770 4. The ASD lambda calculus 774 5. The monadic principle 782 6. Dedekind cuts 788 7. The interval domain in ASD 793 8. The real line as a space in ASD 799 9. Dedekind completeness 803 10. Open, compact and overt intervals 807 11. Arithmetic 812 12. Multiplication 816 13. Reciprocals and roots 821 14. Axiomatic completeness 824 15. Recursive analysis 828 16. Conclusion 832. [ABSTRACT FROM AUTHOR]