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:Category Theory Seminar
SUMMARY:Toposes for modified realizability - Dr. Benno va
n den Berg (University of Amsterdam)
DTSTART;TZID=Europe/London:20191017T141500
DTEND;TZID=Europe/London:20191017T151500
UID:TALK132973AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/132973
DESCRIPTION:One aim of the theory of realizability toposes is
to give a conceptual and semantic account of the v
arious realizability interpretations one can find
in the proof-theoretic literature. But there is no
direct route which goes from a proof-theoretic in
terpretation to its “corresponding” topos. In fact
\, one quickly finds that one has to make some cho
ices on the way. I will discuss some of the issues
that come up when one tries to define a modified
realizability topos. Recall that the proof theoris
t (Kreisel\, Troelstra) will think of modified rea
lizability as an interpretation of arithmetic in f
inite types which validates independence of premis
e and the axiom of choice for all finite types. In
the literature (Van Oosten’s book\, for instance)
one can find a modified realizability topos\, due
to Grayson\, but it does not validate the axiom o
f choice for all finite types. I will discuss two
possible ways in which this can be fixed. If time
permits\, I may even discuss a fourth topos which
also has some claim to being a topos for modified
realizability. (Joint work with Mees de Vries)
LOCATION:MR4\, Centre for Mathematical Sciences
CONTACT:José Siqueira
END:VEVENT
END:VCALENDAR