Steve Vickers: Papers
Below are brief summaries of some of my papers, the most recent first, with links into a more complete bibliography with abstracts, citation details and preprint/postprint versions.
"Sketches for arithmetic universes" sets out a formal categorical account of how geometric theories and their classifing toposes might, in enough cases to be useful, be replaced by a finitary logic and arithmetic universes. This programme was originally proposed in "Topical categories of domains".
"The localic compact interval is an Escardó-Simpson interval object" proves a certain universal property for the localic interval.
(with Christopher Townsend) "A coherent account of geometricity" gives a purely categorical description of the notion of geometric construction on bundles.
(with Bertfried Fauser) "Geometric constructions preserve fibrations" gives a geometricity criterion for bundle constructions to preserve fibrations and opfibrations (in the 2-categorical sense).
(with Francesco Ciraulo) "Positivity relations on a locale" explains the binary positivity relations of Sambin's Basic Picture in more purely localic terms, with reference to algebras for the lower powerlocale.
(with Bas Spitters and Sander Wolters) "Gelfand spectra in Grothendieck toposes using geometric mathematics" uses geometric mathematics to calculate some locales associated with spectral bundles in topos approaches to quantum physics.
"The Born rule as structure of spectral bundles", an extended abstract, outlines how topos approaches to quantum foundations may be understood in terms of a base space of contexts and a bundle where the fibre over a context is its spectrum. The machinery of point-free spaces and geometricty is exploited.
"A monad of valuation locales" develops the mathematics of integration, including Riesz and Fubini theorems, in a localic setting using valuations instead of measures.
"Continuity and geometric logic" gives a broad survey of geometric logic and its unique selling points.
(with Yde Venema and Jacob Vosmaer) "Generalized powerlocales via relation lifting" defines a generalization of the Vietoris powerlocale. For the Vietoris powerlocale itself, the paper gives a new presentation in terms of "nabla", and also proves constructive results regarding compactness.
(with Milly Maietti) "An induction principle for consequence in arithmetic universes" explores some issues, in particular the lack of cartesian closedness, if one uses arithmetic universes instead of Grothendieck toposes to classify (suitable) geometric theories.
(with Achim Jung and Drew Moshier) "Presenting dcpos and dcpo algebras" describes the presentations of dcpo algebras by generators and relations.
"Issues of logic, algebra and topology in ontology" uses geometric logic as a case study for how a logic might be affected by the ontological commitment one is prepared to make.
"Fuzzy sets and geometric logic" describes how geometric logic can provide a conceptual simplification of Hoehle's sheaf approach to fuzzy sets. You can also download slides of my Linz talk on this topic.
"Cosheaves and connectedness in formal topology" gives a predicative introduction to some topos ideas in Bunge and Funk's book "Singular Coverings of Toposes".
"A localic theory of lower and upper integrals" is just what it says.
"The connected Vietoris powerlocale" describes a powerlocale construction whose points are connected, and uses it to give a choice-free constructive account of the Intermediate Value Theorem and Rolle's Theorem.
"Locales and toposes as spaces" is a first step towards a constructive version of "Topology via Logic". It explains how theories in geometric logic can be viewed as topological spaces (for the propositional fragment) or generalized topological spaces (toposes) for the full predicate logic.
(with Erik Palmgren) "Partial Horn logic and cartesian categories" gives a simple presentation of cartesian theories using a logic in which function symbols may be partial. It leads to an easy proof of the free model theorem, and a simple construction of classifying categories.
"Sublocales in formal topology" shows how various results about sublocales in topos-valid locale theory transfer to predicative formal topology.
(with Gillian Hill) "A language for configuring multi-level specifications" develops "Presheaves as configured specifications" to cope with specifications in which components of systems may themselves be configured systems.
"Localic completion of generalized metric spaces I" shows how generalized metric spaces may be completed to give locales. "Generalized" means esentially that only the zero self-distance and the triangle inequality are expected. "Localic completion of generalized metric spaces II: Powerlocales" investigates their powerlocales, gives a simple description of them as "generalized metric powerspaces", and describes some applications.
"Entailment systems for stably locally compact locales" describes a way of presenting stably locally compact locales using a kind of non-reflexive sequent calculus. It is similar to the Multilingual Sequent Calculus of Jung, Kegelmann and Moshier, but without the explicit presence of conjunction and disjunction in the sequents.
(with Christopher Townsend) "A universal characterization of the double powerlocale" shows that the double powerlocale PP(X) can be considered a double exponential $^($^X) even when X is not locally compact (so $X doesn't exist). It does this using the Yoneda embedding of the category of locales.
"Compactness in locales and in formal topology" describes a general criterion for compactness of a formal topology (with preordered base) and proves it in both topos-valid mathematics and predicative mathematics.
"The double powerlocale and exponentiation: a case study in geometric logic" examines the "double powerlocale", the composite of the upper and lower powerlocales, and relates it to exponentiation. It uses geometric reasoning (stable under pullback along geometric morphisms) to make locales appear like spaces.
(with Gillian Hill) "Presheaves as Configured Specifications" outlines a specification language for describing how components are put together with sharing. It uses presheaves to give a mathematical treatment that is both simple and specificationally natural.
"Strongly Algebraic = SFP (Topically)" develops the work of "Topical Categories of Domains" to cover the equivalence between two of Plotkin's characterizations of SFP domains. It also serves as an introduction to how presheaf toposes are interpreted as generalized spaces.
"Localic Completion of Quasimetric Spaces" presents a localic account of completion of quasimetric spaces, using Lawvere's approach by enriched categories.
"Topical Categories of Domains" sets domain theory, and in particular Abramsky's account in "Domain Theory in Logical Form", in a framework of geometric logic. Ordinary categories of domains are replaced by "topical" categories, internal in the category of toposes and geometric morphisms: the classes of objects and morphisms are replaced by toposes classifying them.
"Topology via Constructive Logic" presents the idea that constructive mathematics has practical usefulness in studying topology.
"Constructive points of powerlocales" gives a constructively sound account of the points of the lower, upper and Vietoris powerlocales, and shows how in certain cases a powerlocale of D is homeomorphic to $^D.
"Toposes pour les vraiment nuls" is a further introduction to Grothendieck's idea of toposes as generalized topological spaces, using geometric logic to hide topology.
"Toposes pour les nuls" is a brief introduction to Grothendieck's idea of toposes as generalized topological spaces, written from a topological viewpoint.
"Locales are not pointless" presents some preliminary results for reasoning about arbitrary locales through their points, with particular applications to powerlocales.
(With Mark Dawson) "Towards a GeoZ toolkit" discusses how a mathematical toolkit for GeoZ must differ from that for Z, and illustrates the use of schema entailment in presenting it.
"Geometric logic as a specification language" is a short introduction to GeoZ, a Z-like specification language based on geometric logic. Includes a description of "schema entailment" and its use as a definitional mechanism.
"Geometric Logic in Computer Science" is an introduction to geometric logic, paying particular attention to the deep mathematical properties that make it differ from other logics.
(With Samson Abramsky) "Quantales, Observational Logic and Process Semantics" studies quantales (complete lattices equipped with monoid structure, the binary operation distributing over all joins) with applications to process semantics.
"Information Systems for Continuous Posets" defines an "infosys" as an idempotent relation, and shows how they may be used to present continuous dcpos. Includes a proof that the Vietoris powerlocale of a continuous dcpo is again a continuous dcpo.
"Geometric Theories and Databases" describes a topos-theoretic construction of categorical powerdomains (bagtoposes) with tentative application to database theory.
(With Peter Johnstone) "Preframe Presentations Present" investigates preframes (directed complete posets with finite meets that distribute over the directed joins) with applications to locale theory, including an easy proof of the localic Tychonoff theorem.