BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Toposes for modified realizability  - Dr. Benno van den Berg (Univ
 ersity of Amsterdam)
DTSTART:20191017T131500Z
DTEND:20191017T141500Z
UID:TALK132973@talks.cam.ac.uk
CONTACT:José Siqueira
DESCRIPTION:One aim of the theory of realizability toposes is to give a co
 nceptual and semantic account of the various realizability interpretations
  one can find in the proof-theoretic literature. But there is no direct ro
 ute which goes from a proof-theoretic interpretation to its “correspondi
 ng” topos. In fact\, one quickly finds that one has to make some choices
  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 theorist 
 (Kreisel\, Troelstra) will think of modified realizability as an interpret
 ation of arithmetic in finite types which validates independence of premis
 e and the axiom of choice for all finite types. In the literature (Van Oos
 ten’s book\, for instance) one can find a modified realizability topos\,
  due to Grayson\, but it does not validate the axiom of choice for all fin
 ite 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 clai
 m to being a topos for modified realizability. (Joint work with Mees de Vr
 ies)
LOCATION:MR4\, Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR