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. |
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. |
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. |
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 CCD^{op} (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. |
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.