Girard’s Paradox: Impredicativity Rears its Ugly Head

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.

Oct 19, 2022 12:30 PM — 1:30 PM
Theory Lunch
JCL 298

Join via Zoom