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
|
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.