Equideductive Topology

Paul Taylor

Equideductive topology is a new research programme whose objective, like that of Abstract Stone Duality, is to develop a language for computable general topology. Whilst ASD characterised computably based locally compact spaces, the leading concrete model of equideductive topology is the category of sober topological spaces.

See the Prologue or the announcement on "categories" for a general introduction to the equideductive topology programme.

In addition to the papers below, there is also a cartesian closed extension that is similar to Scott's equilogical spaces. Indeed, the new calculus was developed in answer to the question of what logic is required to perform Scott's construction. However, my notes on this construction are nowhere near being ready for release.

If you have followed my earlier work on either the foundations of ASD or its applications to real analysis you may also like to read my 2009 Prospectus about the motivations for the new programme. Since it replaces the categorical ideas that lay at the foundations of ASD with new ones that are not strict generalisations, the priority in the initial phase it to develop structures that are compatible with the ASD papers as they have been published rather than as they were originally conceived. The ASD programme was supposed to be developed in certain stages but the intermediate ones were not fully documented. The new one will therefore try to follow the plan more strictly, for which reason I intend to prepare drafts of all of the basic papers before I publish any of them.

Equideductive 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]

This first paper studies the interaction between equalisers and exponentials. Categorically, such subspaces are characterised as "partial products".

The logic is a kind of predicate calculus with ∀, ⇒ and & whose object language is the sober λ-calculus. The equivalence between these two formulations is proved.

Although there is a special object Σ, no structure is yet assumed for it.

This work is intended as an alternative to Subspaces in ASD for the foundations that are needed for the applications of ASD.

The Existential Quantifier in Eqduideductive Logic

PDF (294 kb)
DVI (132 kb)
PostScript (compressed) (162 kb)
A5 PS booklet (compressed) (155 kb)
What are these?
[13 Jan 2011]

Although the logic is only defined to have universal quantification, conjunction and equality, it is possible to define an existential quantifier too.

This quantifier agrees with the epis in an equideductive category, which form a factorisation system together with the partial product inclusions. The epis are preserved by products but not by general pullbacks, corresponding to the fact that the rules for the quantifier are subject to severe limitations on the use of variables and in particular do not allow substitution. Such a category also has stable disjoint coproducts.

The only structure that is assumed on Σ for this is a single constant ∗.

This paper begins with a rapid survey of the many different meaning that have been given to the existential quantifier in various forms of symbolic and categorical logic. I would appreciate comments on this historical material as well as on the main subject matter of the paper.

Equideductive Topology

PDF (285 kb)
DVI (121 kb)
PostScript (compressed) (141 kb)
A5 PS booklet (compressed) (133 kb)
What are these?
[20 Feb 2011]

This is the first paper in the equideductive programme that assumes a lattice structure on Σ. It begins from the question of when Σ is a dominance, i.e. it classifies some class of "open" inclusions.

This question leads to an "internal" logic of open subspaces. Discrete, compact, overt and Hausdorff spaces are those form which the external (in)equality or quantifier is represented by a lambda term.

We develop these ideas into a new, two-level, logical calculus for open and general subspaces in computable general topology.

The two levels coincide, i.e. the external logic is always represented by internal structure on Σ ≡ Ω, iff the category is a topos.

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