Equideductive logic and CCCs with subspaces

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

• Paul Taylor
• Thursday 05 February 2009, 14:00-15:00
• Room FW11, Computer Laboratory, William Gates Building.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• Room FW11, Computer Laboratory, William Gates Building
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.