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.

ASD (Abstract Stone Duality) is a re-axiomatisation of general topology in which the topology on a space is treated, not as an infinitary lattice, but as an exponential object of the same category as the original space, with an associated lambda-calculus. In this paper, this is shown to be equivalent to a notion of computable basis for locally compact sober spaces or locales, involving a family of open subspaces and accompanying family of compact ones. This generalises Smyth's effectively given domains and Jung's strong proximity lattices. Part of the data for a basis is the inclusion relation of compact subspaces within open ones, which is formulated in locale theory as the way-below relation on a continuous lattice. The finitary properties of this relation are characterised here, including the Wilker condition for the cover of a compact space by two open ones. The real line is used as a running example, being closely related to Scott's domain of intervals. ASD does not use the category of sets, but the full subcategory of overt discrete objects plays this role; it is an arithmetic universe (pretopos with lists). In particular, we use this subcategory to translate computable bases for classical spaces into objects in the ASD calculus.

Abstract Transitive extensional well founded relations provide an intuitionistic notion of ordinals which admits transfinite induction. However these ordinals are not directed and their successor operation is poorly behaved, leading to problems of functoriality. We show how to make the successor monotone by introducing plumpness, which strengthens transitivity. This clarifies the traditional development of successors and unions, making it intuitionistic; even the (classical) proof of trichotomy is made simpler. The definition is, however, recursive, and, as their name suggests, the plump ordinals grow very rapidly. Directedness must be defined hereditarily. It is orthogonal to the other four conditions, and the lower powerdomain construction is shown to be the universal way of imposing it. We treat ordinals as order-types, and develop a corresponding set theory similar to Osius' transitive set objects. This presents Mostowski's theorem as a reflection of categories, and set-theoretic union is a corollary of the adjoint functor theorem. Mostowski's theorem and the rank for some of the notions of ordinal are formulated and proved without the axiom of replacement, but this seems to be unavoidable for the plump rank. The comparison between sets and toposes is developed as far as the identification of replacement with completeness, and there are some suggestions for further work in this area. Each notion of set or ordinal defines a free algebra for one of the theories discussed by Joyal and Moerdijk, namely joins of a family of arities together with an operation s satisfying conditions such as x ≤ sx, monotonicity or s(x ∨ y) ≤ sx ∨ sy. Finally we discuss the fixed point theorem for a monotone endofunction s of a poset with least element and directed joins. This may be proved under each of a variety of additional hypotheses. We explain why it is unlikely that any notion of ordinal obeying the induction scheme for arbitrary predicates will prove the pure result.

An elementary axiomatization of synthetic domain theory is presented, and it is shown that it is sufficient to deduce the fixed point property and solve domain equations. The aim is to show that an important theorem can be derived from an abstract axiomatization, rather than from a particular model. Also, by providing a common framework in which both PER and classical models can be expressed, this work builds a bridge between the two.>