On 29 June 1997, I announced on "categories" my "Euclidean principle" f(a) & a = f(true) & a which holds for any support classifier or dominance Sigma (ie subobject classifier as in an elementary topos, but for any class of monos, eg open or RE subsets), where a:X->Sigma and f:X x Sigma -> Sigma. I gave a talk about this at the Category Theory meeting in Vancouver that year. At the Category Theory meeting in Tours in 1994 I talked about taking Par\'e's theorem (that the contravariant powerset functor in a topos, which is self-adjoint, is monadic) as an axiom. Another category with this property is the category of locally compact locales, where Sigma is the Sierpinski space and "powerset" means "lattice of open sets", equipped with the Scott topology. This is a way of re-axiomatising general topology without the arbitrary unions in the traditional definition and in locale theory: the category of "frames" is to be both dual to the category of "spaces" and algebraic over it. I have now written up these ideas as a draft paper entitled "An Abstract Stone Duality, I: Geometric and Higher Order Logic" that you can get via my page in the Hypatia Electronic Library, which is http://hypatia.dcs.qmw.ac.uk/author/TaylorP (I sent copies of an earlier draft to a number of people in November 1998, but otherwise this is new text: it is not the same as any "notes on SDT" that you may have got from me over the web in the past.) After some discussion relating the monadic property to sobriety of spaces and spatiality of locales, I prove the converse of the basic observation about the Euclidean principle: if Sigma satisfies it and the adjunction is monadic then Sigma is the classifier for some class of monos. It is neither an axiom nor a theorem that the category has all finite limits. Indeed, the point is that equalisers etc depend on a notion of equality, which, from a computational point of view, is not as straightforward as pure mathematicians have traditionally considered it to be. Some spaces (datatypes) admit equality in a "positive" way: for example in a group given by generators and relations, or in a lambda calculus with reduction rules, we may hope to prove equality of two terms, but not inequality. On the other hand, we may hope to prove inequality of real numbers but not equality. These ideas are formalised by notions of "discrete" and "Hausdorff" spaces respectively, along with definitions of "open" and "compact". We show that the full subcategory of open discrete spaces is a pretopos, the same being true of the compact Hausdorff spaces, by showing that the coequaliser is Sigma-split. The point of Sigma-split co/equalisers is that, being equationally defined, we might hope to be able to compute with them, possibly using something like the "continuation-passing style" used in some compilers. The Euclidean principle and monadicity property are related, respectively, to the Phoa principle and repleteness in sythetic domain theory. In that subject we also need an infinitary axiom that makes all functions Scott continuous and provides fixed points; this axiom is *not* discussed in the present paper, largely because this seemed an appropriate criterion to use to divide up a rambling collection of notes into papers. The infinitary axiom and the construction of the "lift" will be considered in Part II. Under the infinitary axiom, open discrete spaces form an arithmetic universe, ie they admit N-indexed colimits and free algebras, whilst compact Hausdorff space admit limits and cofree coalgebras. You might like to consider this paper alongside the recent work of Alex Simpson and Jaap van Oosten on Synthetic Domain Theory, http://www.math.uu.nl/publications/preprints/1080.ps.gz which is very much concerned with the infinitary axiom. In particular Alex is keen to emphasise the additional completeness of the ambient category that is needed to construct infinitary co/limits and solutions of domain equations, by comparison with directed joins and fixed points of functions. He considers that some attention to the axiom of replacement is needed here, and I agree with him, though our treatments are different. My paper is written for a general mathematical audience, and argues its point of view from a position of extreme Cartesisn doubt. I feel that Alex and Jaap's work is very arcane by comparison, as it depends heavily on Hyland's effective topos. For my own views on replacement, see the final section of my book, Practical Foundations of Mathematics. I hope to be able to make an announcement about the availability of this very soon.
This is a reaction to Paul Taylor's advertisement for his paper on Abstract Stone Duality. Paul has considered appropriate to mention the paper "Axioms and (Counter)examples in Synthetic Domain Theory" by Alex Simpson and myself, and to polemicize against it in the following way:
You might like to consider this paper alongside the recent work of Alex Simpson and Jaap van Oosten on Synthetic Domain Theory, http://www.math.uu.nl/publications/preprints/1080.ps.gz which is very much concerned with the infinitary axiom. In particular Alex is keen to emphasise the additional completeness of the ambient category that is needed to construct infinitary co/limits and solutions of domain equations, by comparison with directed joins and fixed points of functions. He considers that some attention to the axiom of replacement is needed here, and I agree with him, though our treatments are different.
My paper is written for a general mathematical audience, and argues its point of view from a position of extreme Cartesisn doubt. I feel that Alex and Jaap's work is very arcane by comparison, as it depends heavily on Hyland's effective topos.
Thanks, Paul, for mentioning our paper, but since the above text is a blatant misrepresentation of its content, a correction is in order. Our paper develops the theory on the basis of 4 axioms, of which one (the \neg\neg-separatedness of \Sigma) is rather special, as we explicitly acknowledge. Otherwise the treatment is completely general, and "completeness of the ambient category" nowhere enters the picture (we do have, however, some treatment of whether the lift functor preserves internal colimits of chains). The remark about Replacement refers to other work by Alex. The axiomatic treatment raises independence questions, some of which we solve by considering models. One of these models is the effective topos. Nowhere do we hint that the effective topos should have a privileged place among models. Anyway, it is funny that our work, which builds on the tradition of turning SDT into an axiomatic theory (a process which I think is still unfinished), tradition which was started by Pino Rosolini, Wesley Phoa, Martin Hyland and Paul himself, is now found to be "arcane" (mind you, the whole subject is less than twenty years old) by Paul. Jaap van Oosten
participants (2)
-
Jaap van Oosten -
Paul Taylor