Equideductive Topology

Equideductive Topology

[Paul Taylor]

  			Equideductive Topology
  		www.PaulTaylor.EU/ASD/equideductive

Equideductive Topology seeks a new language for computable general topology.

Whereas ASD gave an account of computably based LOCALLY COMPACT spaces,
the leading concrete model of the new theory is the category of all SOBER
topological spaces (in the traditional sense, rather than my abstract one).
Also, the two theories are based on different fundamental categorical ideas.
Whilst they have a lot in common, neither strictly speaking generalises
the other, so it is appropriate to regard this as a NEW research programme.

The word "equideductive" is a double pun on Dana Scott's equilogical spaces
and on reasoning with equations.  One of its motivations was to find out
exactly what kind of logic is needed to construct a cartesian closed
extension of categories of topological spaces.  Indeed, this was the
first piece of work that I did with equideductive logic, but it is still
very unclear to me how the additional spaces behave, so I am nowhere near
ready to release a draft paper about them.

On this occasion, let me concentrate on a way of generalising the INTERNAL
LOGIC OF A TOPOS, otherwise known as naive SET THEORY, to topology.

There is a distinction to be made between the INTERNAL logic that is
encoded by means of "algebraic" structure on Omega such as the quantifiers

         all_X  and  some_X : Omega^X --> Omega

and the EXTERNAL logic of subobjects in the category.   (I would appreciate
help from anyone who has experience of teaching about the internal higher
order logic of a topos regarding how one can put across this distinction.)

By an EXTERNAL LOGIC OF SUBOBJECTS I mean the way in which they are
constructed by means of equalisers and similar basic categorical tools.
(This could perhaps be done in some diagrammatic language based on sketch
theory --- maybe Pierre Ageron's notion of "canevas" would do it.)

In particular, we would like to be able to write

                                                     alpha
                                                     ------>       Y
{ x:X | ALL y:Y. alpha x y = beta x y }  >---->  X         Sigma
                                                     ------>
                                                      beta

for an equaliser targeted at an exponential.   In general topology,
I am thinking of this exponential as being in some cartesian closed
extension, for which the Yoneda embedding is adequate.

If the object  Y  is itself given by such an equaliser then we would
like to use the notation above in a recursive way, eg

{ x:X | ALL y:B.  (ALL z:C.  gamma y z = delta y x)
                     IMPLIES   (alpha x y = beta x y) }.

Such an equaliser targeted at an exponential in an enclosing category
may be described using products instead of exponentials, the universal
property being similar to that known as a "partial product".

The relevant categorical ideas are discussed in my first draft paper,
        "Equideductive Categories and their Logic".
The associated logic is a kind of predicate calculus that uses a
lambda calculus as its object language.

Although the natural symbols of this logic are ALL, IMPLIES, AND and
EQUALS, there is a way of defining a weak existential quantifier (SOME).
This is the subject of the second draft paper.

So far, no internal structure (even lattice operations) has been
assumed for the object Sigma.

The third paper, which introduces the finitary part of Equideductive
Topology itself, begins from the question of when the fundamental
object of an equideductive category is a "dominance".  This means
that it classifies some class of monos in the same way that Omega
does in a topos - in particular uniquely - but not all monos need
be classified.  Those that are we call "open".

The first consequence of this is that Sigma is a semilattice and
its internal order represents the external IMPLIES connective.

We call an equideductive predicate p(x), which is formed from
nested quantified implications between equations as above, "open"
if there is some term phi:Sigma^X such that
       p(x)   -||-    phi x = T

The next step is to ask when the diagonal   X >--> XxX  of an object
(which is an equaliser and therefore defined by an equideductive
predicate) is open.   We say that  X  is a "discrete space" if
there is some term   equals: X x X ---> Sigma   such that
      x = y   -||-    equals x y = T

Next we can ask when the equideductive universal quantifier (ALL)
is represented by a term,  all_X :  Sigma^X ---> Sigma,
      ALL x.(phi x=T)   -||-   (all_X phi) = T
When this happens we say that the object  X  is "compact".
The operation (all_X) may also be seen as an internal "meet"
in the lattice Sigma^X.

Similarly, in an "overt" space X, the equideductive existential
quantifier (SOME) is represented by a term  some_X: Sigma^X --> Sigma
      SOME x.(phi x=T)   -||-   (some_X phi) = T
However, since SOME only obeys a weak form of the rules for the
existential quantifier, it seems better to define (some_X) as
an internal join instead.

The equideductive category is an elementary topos if and only
if all objects are discrete, overt and compact.

Turning to computable general topology, equideductive logic
legitimises and generalises the ad hoc notation that I was
using for non-open (in particular compact) subspaces in ASD.

There is, as I have said, an important distinction to be made
between the external logic of subobjects (given by equalisers etc)
and the internal one on the object Sigma or Omega (given by its
internal algebraic structure).   However, having learned that
distinction one could erase it again.

The interpretation of a formula that makes this distinction ambiguous
is that certain SUB-formulae denote terms in the ASD calculus (with
types such as Sigma or Sigma^X) but the larger formula becomes an
equideductive predicate as soon as one of the rules is broken:

-  "equals" stays within the term calculus if it links terms whose
     type is discrete, but otherwise yields an equideductive predicate;

- likewise "not-equals" for Hausdorff type

- "all" stays within the term calculus if it is applied to a term
    and its range is a compact type, otherwise it gives a predicate;

- likewise "some" for overt type.

Looking forward to your comments,

Paul Taylor


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]