The Dedekind Reals in Abstract Stone Duality

Andrej Bauer and Paul Taylor

article{TaylorP:dedras,
  author = {Bauer, Andrej and Taylor, Paul},
  title = {The {D}edekind Reals in Abstract {S}tone Duality},
  journal = {Mathematical Structures in Computer Science},
  publisher = {Cambridge University Press},
  year = 2009,
  volume = 19,
  pages = {757--838},
  doi = {10.1017/S0960129509007695},
  url = {PaulTaylor.EU/ASD/dedras/},
  amsclass = {03F60, 06E15, 18C20, 26E40, 54D45, 65G40}}
Published online 8 June 2009.
Abstract
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.


History
This paper was presented at It has been accepted by the referees for a journal (details to follow).
Acknowledgements
This paper is the result of a collaboration that began during Paul Taylor's visit to Ljubljana in November 2004. It was presented at Computability and Complexity in Analysis in Kyoto on 28 August 2005, and we are grateful to Peter Hertling and the CCA programme committee for the indulgence of allowing us to occupy altogether 80 pages of their proceedings.
We would also like to thank Vasco Brattka, Douglas Bridges, Fer-Jan de Vries, Peter Johnstone, Andrea Schalk, Peter Schuster, Alex Simpson, Maarten van Emden and Graham White for their helpful comments, and the anonymous referee for a most professional report.
The top-level HTML pages on this site (including this one) were translated from LATEX using TTH, whilst Hevea was used for the content of this paper.
Download the paper to print it
PDF,    DVI,    compressed PostScript    or    A5 booklet.

Table of contents and the HTML version
Classical overview
In traditional notation; not part of the journal paper.
1. Introduction
Our axioms; the Heine-Borel theorem in various constructive theories.
2. Cuts and intervals
Generalising Dedekind cuts to intervals; Moore's operations; extending funtions and predicates; the E operator classically; fundamental theorem of interval analysis; back-to-front intervals.
3. Topology as lambda-calculus
Overview of Abstract Stone Duality.
4. The ASD lambda calculus
A "user manual": types, terms, propositions, statements, judgements; Gentzen and Phoa rules; classifying open and closed subspaces; discrete, Hausdorff, compact and overt spaces, with examples; definition by description; directed joins; Scott continuity.
5. The monadic principle
Σ-split subspaces; nuclei; admissibility; open and closed subspaces; the type-theoretic rules; constructions in other papers; the monadic principle.
6. Dedekind cuts
Dense linear orders without endpoints; Dedekind cuts; order relations.
7. The interval domain in ASD
Constructions of the ascending and descend reals, and of the unbounded and bounded interval domains, using nuclei.
8. The real line as a space in ASD
Construction of the real line using the nucleus E.
9. Dedekind completeness
R is overt, Hausdorff, totally ordered and Dedekind complete; binary min and max; negation and absolute value.
10. Open, compact and overt intervals
Construction of the open and closed intervals; these are both overt; the closed interval is compact; finite open sub-covers.
11. Arithmetic
Scheme for extending the arithmetic operations; roundedness of the Moore operations; addition of intervals; the Archimedean principle; additive locatedness.
12. Multiplication
Approximate division; roundedness of Moore multiplication; multiplication of intervals; locateness; conjecture re non-Archimedean recursive Conway numbers.
13. Reciprocals and roots
Strictly monotone graphs; inverse functions; reciprocals; roots; logarithms and exponentials.
14. Axiomatic completeness
Traditional proof of uniqueness of Dedekind reals; uniqueness of their topology without assuming completeness; sobriety; rules for Dedekind cuts and R as a primitive type; conservativity.
15. Recursive analysis
Singular covers and the failure of Heine-Borel in Recursive Analysis; bringing the results into confrontation; PERs and the effective topos; the monadic completion of a model.
15. Conclusion
References

This is www.PaulTaylor.EU/ASD/dedras/index.html and it was derived from ASD/dedras.tex which was last modified on 16 July 2009.