Inside every model of Abstract Stone Duality lies an Arithmetic Universe

Paul Taylor

This is part of the core theory of Abstract Stone Duality for locally compact spaces. It was published in Electronic Notes in Theoretical Computer Science 122, 247–296 in 2005 (BibTeX).



The first paper published on Abstract Stone Duality showed that the overt discrete objects (those admitting ∃ and = internally) form a pretopos, i.e. a category with finite limits, stable disjoint coproducts and stable effective quotients of equivalence relations. Using an N-indexed least fixed point axiom, here we show that this full subcategory is an arithmetic universe, having a free semilattice (“collection of Kuratowski-finite subsets”) and a free monoid (“collection of lists”) on any overt discrete object. Each finite subset is represented by its pair ([], <>) of modal operators, although a tight correspondence with these depends on a stronger Scott-continuity axiom. Topologically, such subsets are both compact and open and also involve proper open maps. In applications of ASD this can eliminate lists in favour of a continuation-passing interpretation.



Acknowledgements

I would like to thank Peter Aczel, Andrej Bauer, Robin Cockett, Maria Emilia Maietti and Gavin Wraith for their helpful comments. This paper was accepted for Category Theory and Computer Science 10, which was held in Copenhagen in August 2004, and an abridged version appeared in the printed proceedings. However, I was unable to attend, as I had broken my leg two weeks earlier.

BibTeX entry

   @article{TaylorP:insema,
      author    = {Taylor, Paul},
      title     = {Inside every model of Abstract Stone Duality
                   lies an Arithmetic Universe},
      journal   = {Electronic Notes in Theoretical Computer Science},
      publisher = {Elsevier},
      year      = 2005,
      volume    = 122, pages = {247--296},
      url       = {PaulTaylor.EU/ASD/insema}}

Download the paper to print it

PDF,  DVI,  compressed PostScript  or  A5 booklet.




Table of contents


1. Introduction


2. Proofs and natural numbers in ASD


3. Finite subsets as modal operators


4. Fixed point properties


5. Stages in the construction


6. Admissible implies modal


7. K as a functor


8. Lists, heads and tails


9. Recursion over lists


10. The free semilattice


11. Overt compact subspaces


References

This document was translated from LATEX by HEVEA.