BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:On relating strong type theories and set theories - Rathjen\, M (U
 niversity of Leeds)
DTSTART:20151215T100000Z
DTEND:20151215T110000Z
UID:TALK62904@talks.cam.ac.uk
CONTACT:42080
DESCRIPTION:There exists a fairly tight fit between type theories  la Mart
 in-Lf and constructive set theories such as CZF and its extension\, and th
 ere are connections to classical Kripke-Platek set theory and extensions t
 hereof\, too. The technology for determining the (exact) proof-theoretic s
 trength of such theories was developed in the late 20th century. The situa
 tion is rather different when it comes to type theories (with universes) h
 aving the impredicative type of propositions Prop from the Calculus of Con
 structions that features in some powerful proof assistants. Aczel's sets-a
 s-types interpretation into these type theories gives rise to rather unusu
 al set-theoretic axioms: negative power set and negative separation. But i
 t is not known how to determine the consistency strength of intuitionistic
  set theories with such axioms via familiar classical 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 kno
 wn results from this area. The second part will be concerned with the rath
 er special computational and proof-theoretic behavior of such theories.\n
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR