University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Equideductive logic and CCCs with subspaces

Equideductive logic and CCCs with subspaces

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Sam Staton.

NOTE UNUSUAL DAY.

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 .

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity