Equideductive Topology

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^AT_EX by H^EV^EA.