BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Equideductive logic and CCCs with subspaces - Paul Taylor
DTSTART:20090205T140000Z
DTEND:20090205T150000Z
UID:TALK15664@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:In any cartesian closed category with equalisers\, the logic o
 f regular\nmonos (maps that arise as equalisers) of course has conjunction
 s.\nBut also\, if p(x) represents a regular mono into X and f\,g: X x Y --
 > Z\nare any maps then there is a regular mono into Y represented by\nq(y)
  =  All x. p(x) ==> f(x\,y) = g(x\,y).   Categorically\, q(y) can\nbe defi
 ned by a kind of partial product.\n\nThis apparently rather feeble logic i
 s nevertheless interesting\nfor a number of reasons:\n\nIt is how we reaso
 n with proofs of equations in algebra\, ie treating\njudgements that one e
 quation follows from others\, proof rules about\nsuch judgements (such as 
 induction schemes)\, etc.\, as arbitrarily\nnestable implications.\n\nIt m
 ay be interpreted in the category of sober topological spaces\,\nand maybe
  locales.\n\nTogether with the lattice structure on the Sierpinski space a
 nd an\naxiom that identifies equideductive implication with the lattice or
 der\,\nit is the logic that is needed to form open\, closed\, compact and\
 novert subspaces in ASD.\n\nIt provides the abstract (type-theoretic) basi
 s on which to construct\na cartesian closed category with equalisers simil
 ar to Scott's\nequilogical spaces.\n\nHowever\, the logical formulae that 
 are generated when working with it\nget complicated\, and seem to need ano
 ther simplifying axiom\, for\nwhich I have a candidate.  This raises the i
 ssue of consistency\,\nbut the weakness of equideductive logic is its stre
 ngth:  it has a\nrealisability interpretion in itself\, which ought to pro
 vide a tool\nfor proving conservativity of extensions\,  but I need some h
 elp to\ndo this.\n\nMore on abstract stone duality at Paul's web page: "ww
 w.PaulTaylor.EU/ASD":http://www.PaulTaylor.EU/ASD .\n\nThe slides are at \
 n"PaulTaylor.EU/slides/#09-Cambridge":http://www.PaulTaylor.EU/slides/#09-
 Cambridge .
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR