Geometric and Higher Order Logic

Paul Taylor

This is part of the core theory of Abstract Stone Duality for locally compact spaces. It was published in Theory and Applications of Categories 7(15), 284–338 in December 2000 (BibTeX).



The contravariant powerset and its generalisations ΣX to the lattices of open subsets of a locally compact topological space and of recursively enumerable subsets of numbers satisfy the Euclidean principle that σ∧ F(σ)⇔ σ∧ F(⊤).

Conversely, when the adjunction Σ(−)⊣Σ(−) is monadic, this equation implies that Σ classifies some class of monos and the Frobenius law ∃ x.(φ(x)∧ψ)⇔ (∃ x.φ(x))∧ψ for the existential quantifier.

In topology, the lattice duals of these equations also hold, and are related to the Phoa principle in synthetic domain theory.

The natural definitions of discrete and Hausdorff spaces correspond to equality and inequality, whilst the quantifiers considered as adjoints characterise open (or, as we call them, overt) and compact spaces. Our treatment of overt discrete spaces and open maps is precisely dual to that of compact Hausdorff spaces and proper maps.

The category of overt discrete spaces forms a pretopos. The paper concludes with a converse of Paré’s theorem (that the contravariant powerset functor is monadic) that characterises elementary toposes by means of the monadic and Euclidean properties together with all quantifiers, making no reference to subsets.


This was chronologically the first paper in the Abstract Stone Duality programme, which has this evolved quite considerably in the intervening years. This version therefore contains numerous annotations that explain how the ideas developed, or didn’t develop. The notation has been made to conform to that adopted in later work and minor corrections have been made without comment. However, significant comments and modifications are indicated by square brackets.



Acknowledgements

The original inspiration for this work came while I was visiting Pino Rosolini at the Università degli Studi di Genova in March 1993, and many of the results were found during my second visit in October and November 1997; both visits were funded by the Italian Concilio Nazionale della Ricerca.

This paper was drafted during my visit to Macquarie University in August 1997.

The work has benefitted much from my discussions with Martín Escardó, Martin Hyland, Peter Johnstone, Anders Kock, Eugenio Moggi, Bob Paré, Bob Rosebrugh, Pino Rosolini, Andrea Schalk, Alex Simpson, Thomas Streicher, Steve Vickers, Graham White, Todd Wilson and Richard Wood.

The Euclidean principle was announced in the categories electronic mail forum on 29 June 1997, but I had first encountered this equation on 12 March 1997.


BibTeX entry

   @article{TaylorP:subasd,
      author    = {Taylor, Paul},
      title     = {Geometric and Higher Order Logic
                   in terms of Abstract Stone Duality},
      journal   = {Theory and Applications of Categories},
      publisher = {Mount Allison University},
      year      = 2000, month = {December},
      volume    = 7, number = 13=5, pages = {284--338},
      url       = {PaulTaylor.EU/ASD/geohol},
      amsclass  = {03F35, 06D22, 06E15, 18A15, 18B05,
                   18C20, 54A05, 54D10, 54D30, 54D45}}

Download the paper to print it

PDF,  DVI,  compressed PostScript  or  A5 booklet.




Table of contents


1. Introduction


2. Support classifiers


3. The Euclidean principle


4. The origins of the Euclidean principle


5. The Phoa principle


6. Discrete and Hausdorff objects


7. Overt and compact objects


8. The quantifiers


9. Unions and coproducts


10. Open discrete equivalence relations


11. Monadicity for elementary toposes


References

This document was translated from LATEX by HEVEA.