Nathan Mull, University of Chicago
Girard’s Paradox is often described as a type-theoretic analog of Russell’s paradox. In essence, it says that if you want to use your type theory as a logic, there can be no type of all types. But wait, didn’t type theory come to the rescue in the aftermath of Russell’s paradox? Though, come to think of it, if we can’t have a set of all sets, why would we think there could be a type of all types? And you’re telling me Girard’s paradox applies to systems without a type of all types? Also, what’s type theory? In this talk, I’ll try to address some of these questions.
Join via Zoom