Abstract Stone Duality beyond Local Compactness

Paul Taylor

25 June 2009

Abstract Stone Duality is a new paradigm for General Topology that re-formulates it in a constructive and computable way, using axioms that are about topology and not set theory. The established core of the theory has given an account of computably based locally compact spaces. This was applied to elementary real analysis, yielding a recursive model of the real line in which [0,1] is compact, contrary to the received wisdom based on Russian Recursive Analysis.
The draft papers on this page concern two tentative extensions of the theory that take it beyond local compactness. Beware that these have not, as yet, been made compatible with either the core theory or each other, but I mean this in the weak software sense of compatibility, not the strong mathematical one that there is any evidence of inconsistency.

Equideductive Logic

Equideductive logic is a weak higher order predicate calculus whose object language is the sober lambda-calculus. This is a natural setting in which to express proof rules (such as those that define compactness and overtness) and generalise them.
The leading model is the category of sober topological spaces.
This logic can be used to construct a cartesian closed category similar to Dana Scott's equilogical spaces.
The most striking aspect of it is the new weak existential quantifier, which characterises epis that are stable under products but not necessarily pullbacks.
I presented preliminary versions of this work at conferences at Sussex and Padova and at a seminar in Cambridge. There is also a summary in the last section of Foundations for Computable Topology.

Eqduideductive Categories and their Logic

PDF (821 kb)
DVI (423 kb)
PostScript (compressed) (650 kb)
A5 PS booklet (compressed) (651 kb)
What are these?
[22 Aug 2013]
An equideductive category is one that lies in a nice way within its cartesian closed extensions, examples being the categories of sets, sober topological spaces and affine varieties, but not locales.
Equideductive logic is a kind of predicate calculus in which to reason about the subobjects of such a category. Its most striking aspect of it is the new weak existential quantifier, which characterises epis that are stable under products but not necessarily pullbacks.
In a topos, the logic is equivalent to the higher order logic of the subobject classifier, but, whilst our logic also uses a special object, no structure is assumed for it, and it is not the source of the logic.
The topological and set-theoretic cases are recovered by requiring respectively some or all of the new quantifiers to agree with structure on the key object.

Cartesian Closed Categories with Subspaces

This paper is not available to download.
We study the construction and axiomatisation of categories that have finite limits, exponentials and a subccc of objects that are injective with respect to their own subspaces. This leads to generalisations of Scott's equilogical spaces. We characterise the categories that are obtained in this way by means of an exactness property.
I expect to be able to make a draft of this paper available shortly.

Realisability for Eqduideductive Logic

This paper is not available to download. Equideductive logic is a very weak predicate calculus with implication and universal quantification whose object language is a simply typed lambda-calculus. By considering a realisability interpretation of the proofs in this logic in its underlying lambda calculus, we show that, if a term of ground type can be deduced from a universally quantified hypothesis, then it may also be deduced from this hypothesis quantified over some compact subspace. We use this to consider analogues of the adjoint function theorem and conservativity of an additional principle for equideductive logic. This is applied to constructing a variant of Scott's category of equilogical space that has better categorical exactness properties.
This is not even a draft paper since it contains many blatant gaps. It is a discussion document that I have circulated privately, resulting in some very interesting feedback from a proof theorist.

Underlying sets

In classical general topology, the underlying set functor has adjoints on both sides that assign respectively the discrete and indiscriminate topologies to a set. In ASD, the full subcategory of overt discrete objects plays the role of sets and the leftmost of these functors. So the idea of the work below is that this inclusion have a right adjoint, the underlying set functor, which assigns an overt discrete object to each object of the category. The subcategory then becomes a topos.
There is a summary of this in Foundations for Computable Topology.

An Elementary Theory of Various Categories of Spaces in Topology

PDF (594 kb)
DVI (283 kb)
PostScript (compressed) (203 kb)
A5 PS booklet (compressed) (191 kb)
What are these?
[12 Feb 2009] 		November 2004. Still in very much a draft state.
This was presented at Foundational Methods in Computer Science, University of British Columbia 2-5 June 2005.
In Abstract Stone Duality the topology on a space X is treated, not as an infinitary lattice, but as an exponential space ΣX. This has an associated lambda calculus, in which monadicity of the self-adjunction Σ− −| Σ− makes all spaces sober and gives subspaces the subspace topology, and the Euclidean principle Fσ∧σ = FT∧σ makes Σ the classifier for open subspaces. Computably based locally compact locales provide the leading model for these axioms, although the methods are also applicable to CCDop (constructively completely distributive lattices).
In this paper we recover the textbook theories, using the additional axiom that the subcategory of overt discrete objects have a coreflection, the "underlying set" functor. This subcategory is then a topos, and the whole category is characterised in the minimal situation as that of locally compact locales over that topos.
However, by adding further axioms regarding the existence of equalisers and injectivity of Σ, we find the category of sober spaces or of locales over the topos as a reflective subcategory, whilst the whole category is cartesian closed and has all finite limits and colimits.
Instead of building cartesian closed extensions of the textbook categories by traditional set-theoretic methods, all of these categories (and their underlying topos) are developed entirely synthetically from the ASD lambda calculus, which is therefore logically complete. The methods are briefly applied to give a synthetic explanation of a topology on the set of continuous functions that has been known since the 1970s and satisfies the β- but not the η-law.
We conclude with a proposal for a new theory (in categorical and symbolic form) for a cartesian closed category for recursive topology.
This paper therefore puts the study of topological spaces and locales on a new foundation, just as elementary toposes did for sets.

An Elementary Theory of the Category of Locally Compact Locales

This paper is not available to download. This is the original version of the previous paper. It was presented at the APPSEM Workshop in Nottingham in March 2003.

This is www.PaulTaylor.EU/ASD/extension.php and it was derived from ASD/extension.tex which was last modified on 20 February 2011.