## Equideductive Topology## Paul Taylor |

We introduce a new, two-level, logical calculus for open and general subspaces in computable general topology. The leading model is the category of all sober topological spaces.

In *Equideductive Categories and their Logic*
the “external” logic was motivated by equalisers
targeted at exponentials in an enclosing cartesian closed category.
It was developed into a “predicate calculus” with
universally quantified implications between equations between lambda terms.
A kind of existential quantifier may also be defined.

Here we ask when the fundamental object of this category is a dominance and show how this question leads to an “internal” logic of open subspaces. Discrete, compact, overt and Hausdorff spaces are those form which the external (in)equality or quantifier is represented by a lambda term.

In particular, the category is a topos if this representation
always exists, *i.e*. the external and internal logics coincide.

**Download the paper to print it**

PDF, DVI, compressed PostScript or A5 booklet.

This document was translated from L^{A}T_{E}X byH^{E}V^{E}A.