#
Geometric and Higher Order Logic in terms of Abstract Stone Duality

##
Paul Taylor

The contravariant powerset, and its generalisations $\Sigma^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 $\phi\meet F(\phi)=\phi\meet F(\top)$.

Conversely, when the adjunction $\Sigma^{(-)}\dashv\Sigma^{(-)}$ is
monadic, this equation implies that $\Sigma$ classifies some class
of monos, and the Frobenius law
$\exists x.(\phi(x)\meet\psi)=(\exists x.\phi(x))\meet\psi)$
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 and 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.

Keywords: locally compact spaces; compact Hausdor. spaces, open spaces; overt spaces;
open maps; proper maps; higher order logic; contravariant powerset; elementary topos;
subobject classifier; Euclidean principle; synthetic domain theory; monadic adjunction; pretopos; quantifiers.

2000 MSC: 03F35 06D22 06E15 18A15 18B05 18C20 54A05 54C10, 54D10 54D30 54D45.

*Theory and Applications of Categories*, Vol. 7, 2000, No. 15, pp 284-338.

http://www.tac.mta.ca/tac/volumes/7/n15/n15.dvi

http://www.tac.mta.ca/tac/volumes/7/n15/n15.ps

http://www.tac.mta.ca/tac/volumes/7/n15/n15.pdf

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/7/n15/n15.dvi

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/7/n15/n15.ps

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/7/n15/n15.pdf

TAC Home