From intuitionism to synthetic homotopy theory

Add to your list(s) Download to your calendar using vCal

• Sean Moss, DPMMS
• Monday 17 October 2016, 16:20-17:00
• MR3, CMS.

If you have a question about this talk, please contact Jack Smith.

Intuitionistic logic, based on the philosophy of Intuitionism, is often summarized as proof without the Law of the Excluded Middle. An intuitionistic proof carries constructive information about its conclusion, and different proofs will yield different such information. This is a mathematics where the proofs themselves matter more than the mere truth of propositions. I will discuss how the idea of proof-relevant mathematics has evolved into the new field of Homotopy Type Theory, which is intended to be a new formal foundation for mathematics and, miraculously, supports a kind of synthetic (or axiomatic) version of the homotopy theory of spaces.

This talk is part of the DPMMS PhD student colloquium series.

This talk is included in these lists:

• All CMS events
• CMS Events
• DPMMS PhD student colloquium
• DPMMS info aggregator
• Hanchen DaDaDash
• Interested Talks
• MR3, CMS
• bld31

Note that ex-directory lists are not shown.