# Real Analysis in Abstract Stone Duality

### Paul Taylor

Abstract Stone Duality is a new paradigm for general topology and real analysis that is based directly on continuous functions and predicates, and not sets. It is both constructive and computable, but its idioms of reasoning often look like a sanitised form of classical logic. The papers below on real analysis currently provide the best introduction to ASD. The core theory is developed in the papers on locally compact spaces, but these rely on a deeper understanding of categorical techniques.

### Axioms for the real line

The real line and its topology are characterised uniquely by the following properties:
• R is an overt space, with an existential quantifier ∃;
• it is Hausdorff, with an inequality or apartness relation, ≠ ;
• the closed interval [0,1] is compact, with a universal quantifier ∀x:[0,1];
• R has a total order, i.e. (xy)   ⇔   (x < y) ∨(y < x);
• it is Dedekind complete, in a sense in which the two halves of a cut are open;
• it is a field, where x−1 is defined iff x ≠ 0; and
• Archimedean, i.ey > 0    ⇒   ∃n:Z. y(n−1) < x < y(n+1).
Each of the papers (separately) explains what these axioms (and those of the wider theory) mean formally.
The syntactic language that this description provides may be roughly summed up in the following table of operations:
 arguments:
 variables
 constants
 N
 R
 N&Σ
 R&Σ
 N&?
 Σ
 results:
 N
 k,n,m
 0
 +×
 rec
 the
 R
 a,b,x,y,z
 0,1
 n
 +−×÷
 rec
 cut
 Σ
 δ,υ,φ,ψ
 T,⊥
 = ≤ ≥ < > ≠
 < > ≠
 ∃n
 ∃x:R,∀x:[a,b]
 rec
 ∧,∨
in which Σ is the Sierpinski space, rec is primitive recursion over N at all types, the is definition by description and cut defines real numbers by Dedekind cuts.
Logically, terms of type Σ are semi-decidable properties. That is, if the property is true then you will (eventually) find this out, but you will never be told that it fails.

### Which paper should I read first?

Each of the following papers has been written independently of the others, and provides an introduction to ASD that is suitable for a particular audience. So, depending on your background, you should read
Some of the papers are available in HTML for on-screen browsing; in these cases the title has a hyper-link.

### A Lambda Calculus for Real Analysis

 PDF (818 kb) DVI (654 kb) PostScript (compressed) (471 kb) A5 PS booklet (compressed) (445 kb) What are these?[19 Aug 2010] Presented at Computability and Complexity in Analysis, Kyoto, 25-29 August 2005, using these slides; Canadian Mathematical Society Summer Meeting, Calgary, 3-5 June 2006, using these improved slides; and Third Workshop on Formal Topology, Padova, 7-12 May 2007, using these new slides. This paper is intended for the general mathematician. It introdes the ASD axioms above for R and applies them to elementary real analysis. In particular, it studies the Intermediate Value Theorem, i.e. the solution of equations f x=0 for continuous f:R→R, and the notion of connectedness that is abstracted from it. In classical real analysis thie theorem holds for general continuous functions. However, it is well known from both numerical and constructive considerations that the equation cannot be solved if f "hovers" near 0, whilst tangential solutions will never be found. The paper begins with a summary of the constructive critique, but goes on to throw new light on the cases that constructivists usually dismiss. In ASD, both of these failures and the general method of finding solutions of the equation when they exist are explained by the new concept of "overtness". The zeroes are captured, not as a set, but by higher-type operators [] and < > that remain (Scott) continuous across singularities of a parametric equation. Expressing topology in terms of continuous functions rather than sets of points leads to a very closely dual treatment of open and closed subspaces, without the double negations of intuitionistic approaches. In this, the dual of compactness is overtness, and whereas meets and joins in locale theory are asymmetrically finite and infinite, they have overt and compact indices in ASD. Overtness replaces metrical properties such as total boundedness, and cardinality conditions such as having a countable dense subset. It is also related to locatedness in constructive analysis and recursive enumerability in recursion theory. As a further application of connectedness, we also show that every open set of the line is uniquely expressible as a countable union of intervals, in a suitable constructive sense, which is not the case in Bishop's theory. The characterisation of open subsets of R as countable unions of disjoint open intervals, and some counterexamples, were added in April 2007; these are in (the present) Sections 13, 15 and 16. In this, the January 2008 version, Sections 3, 5, 6, 7, 9 and 10 have been completely (re)written to provide a brief Òneed to knowÓ account of various foundational disciplines that underlie this work.

### The Dedekind Reals in Abstract Stone Duality

 PDF (764 kb) DVI (550 kb) PostScript (compressed) (447 kb) A5 PS booklet (compressed) (425 kb) What are these?[03 Jun 2009] with Andrej Bauer. Mathematical Structures in Computer Science, 19 (2009) 757-838. Presented at Computability and Complexity in Analysis, Kyoto, 25-29 August 2005, using these slides. Also presented at Foundational Methods in Computer Science, Kananaskis, Canadian Rockies, 7-9 June 2006, using these improved slides. 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, it is founded on the algebra of open subspaces. ASD is presented as a λ-calculus, of which this paper provides 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, these concepts being defined in ASD 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. Our definitions of the arithmetic operations are more complicated than Moore's, because we work constructively. The final section compares ASD with other systems of constructive and computable topology and analysis.

### Interval Analysis Without Intervals

 PDF (315 kb) DVI (114 kb) PostScript (compressed) (102 kb) A5 PS booklet (compressed) (95 kb) What are these?[12 Feb 2009] The slides that I used for my presentation at Real Numbers and Computers (Nancy, 10-12 July 2006) give a more complete account of this work. The paper is incomplete. We argue that Dedekind completeness and the Heine-Borel property should be seen as part of the "algebraic" structure of the real line, along with the usual arithmetic operations and relations. Dedekind cuts provide a uniform and natural way of formulating differentiation, integration and limits. They and these examples also generalise to intervals. Together with the arithmetic order, cuts enjoy proof-theoretic introduction and elimination rules similar to those for lambda abstraction and application. This system completely axiomatises computably continuous functions on the real line. We show how this calculus (of "single" points) can be translated formally into Interval Analysis, interpreting the arithmetic operations a la Moore, and compactness as optimisation under constraints. Notice that interval computation is the conclusion and not the starting point.

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