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:Isaac Newton Institute Seminar Series
SUMMARY:On relating strong type theories and set theories
- Rathjen\, M (University of Leeds)
DTSTART;TZID=Europe/London:20151215T100000
DTEND;TZID=Europe/London:20151215T110000
UID:TALK62904AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/62904
DESCRIPTION:There exists a fairly tight fit between type theor
ies la Martin-Lf and constructive set theories su
ch as CZF and its extension\, and there are connec
tions to classical Kripke-Platek set theory and ex
tensions thereof\, too. The technology for determi
ning the (exact) proof-theoretic strength of such
theories was developed in the late 20th century. T
he situation is rather different when it comes to
type theories (with universes) having the impredic
ative type of propositions Prop from the Calculus
of Constructions that features in some powerful pr
oof assistants. Aczel's sets-as-types interpretati
on into these type theories gives rise to rather u
nusual set-theoretic axioms: negative power set an
d negative separation. But it is not known how to
determine the consistency strength of intuitionist
ic set theories with such axioms via familiar clas
sical set theories (though it is not difficult to
see that ZFC plus infinitely many inaccessibles pr
ovides an upper bound). The first part of the talk
will be a survey of known results from this area.
The second part will be concerned with the rather
special computational and proof-theoretic behavio
r of such theories.\n
LOCATION:Seminar Room 1\, Newton Institute
CONTACT:
END:VEVENT
END:VCALENDAR