Event Detail

Type theory, originally conceived as a bulwark against the paradoxes of naive set theory, has languished for a long time in the shadow of axiomatic set theory which became the mainstream foundation of mathematics in the 20th century. But type theories, especially dependent ones à la Martin-Löf, are looked upon favorably these days. The recent renaissance not only champions type theory as a central framework for constructive mathematics and as an important tool for achieving the goal of fully formalized mathematics (amenable to verification by computer-based proof assistants) but also finds deep and unexpected connections between type theory and other areas of mathematics. One aspect, though, that makes type theories irksome is their overbearing syntax and rigidity. It is probably less known that they can often be related to set theories, albeit intuitionistic ones, and thereby rendered more accessible to those who favor breathing ``set-theoretic” air, as it were (like the speaker). This connection was first unearthed by Peter Aczel in the previous century. Still, intuitionistic set theories can behave in rather unexpected ways and it is often surprising to find out which classical set theories they relate to. This and more recent developments will constitute the main bulk of the talk.