BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:Equideductive logic and CCCs with subspaces - Paul
Taylor
DTSTART;TZID=Europe/London:20090205T140000
DTEND;TZID=Europe/London:20090205T150000
UID:TALK15664AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/15664
DESCRIPTION:In any cartesian closed category with equalisers\,
the logic of regular\nmonos (maps that arise as e
qualisers) of course has conjunctions.\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 regula
r mono into Y represented by\nq(y) = All x. p(x)
==> f(x\,y) = g(x\,y). Categorically\, q(y) can\
nbe defined by a kind of partial product.\n\nThis
apparently rather feeble logic is nevertheless int
eresting\nfor a number of reasons:\n\nIt is how we
reason with proofs of equations in algebra\, ie t
reating\njudgements that one equation follows from
others\, proof rules about\nsuch judgements (such
as induction schemes)\, etc.\, as arbitrarily\nne
stable implications.\n\nIt may be interpreted in t
he category of sober topological spaces\,\nand may
be locales.\n\nTogether with the lattice structure
on the Sierpinski space and an\naxiom that identi
fies 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) basis
on which to construct\na cartesian closed category
with equalisers similar to Scott's\nequilogical s
paces.\n\nHowever\, the logical formulae that are
generated when working with it\nget complicated\,
and seem to need another simplifying axiom\, for\n
which I have a candidate. This raises the issue o
f consistency\,\nbut the weakness of equideductive
logic is its strength: it has a\nrealisability i
nterpretion in itself\, which ought to provide a t
ool\nfor proving conservativity of extensions\, b
ut I need some help to\ndo this.\n\nMore on abstra
ct stone duality at Paul's web page: "www.PaulTayl
or.EU/ASD":http://www.PaulTaylor.EU/ASD .\n\nThe s
lides are at \n"PaulTaylor.EU/slides/#09-Cambridge
":http://www.PaulTaylor.EU/slides/#09-Cambridge .
LOCATION:Room FW11\, Computer Laboratory\, William Gates Bu
ilding
CONTACT:Sam Staton
END:VEVENT
END:VCALENDAR