Abstract

In any cartesian closed category with equalisers, the logic of regular monos (maps that arise as equalisers) of course has conjunctions. But also, if p(x) represents a regular mono into X and f,g: X x Y—> Z are any maps then there is a regular mono into Y represented by q(y) = All x. p(x) ==> f(x,y) = g(x,y). Categorically, q(y) can be defined by a kind of partial product.

This apparently rather feeble logic is nevertheless interesting for a number of reasons:

It is how we reason with proofs of equations in algebra, ie treating judgements that one equation follows from others, proof rules about such judgements (such as induction schemes), etc., as arbitrarily nestable implications.

It may be interpreted in the category of sober topological spaces, and maybe locales.

Together with the lattice structure on the Sierpinski space and an axiom that identifies equideductive implication with the lattice order, it is the logic that is needed to form open, closed, compact and overt subspaces in ASD .

It provides the abstract (type-theoretic) basis on which to construct a cartesian closed category with equalisers similar to Scott’s equilogical spaces.

However, the logical formulae that are generated when working with it get complicated, and seem to need another simplifying axiom, for which I have a candidate. This raises the issue of consistency, but the weakness of equideductive logic is its strength: it has a realisability interpretion in itself, which ought to provide a tool for proving conservativity of extensions, but I need some help to do this.

More on abstract stone duality at Paul’s web page: www.PaulTaylor.EU/ASD .

The slides are at PaulTaylor.EU/slides/#09-Cambridge .