Talk:Type theory

All Logical Roads Lead to Rome

I propose a section discussing the two different approaches to resolving Russell's paradox: (1) Zermelo's approach - place restrictions on comprehension leading to the canonical ZF or ZFC, or (2) Russell's approach - ban impredicative concepts leading to Type Theoretic Set Theories. This section would highlight the consensus opinion (among mathematicians) of the superiority of ZF or ZFC; the difficulties of Type Theories. But is there an alternative...that preserves our intuitions? Yes! New Foundations and NFU. They resolve Russell's paradox whilst allowing the use of a Universal Set ξ. Leucippus 02:38, 17 December 2020 (UTC)