Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Created Russell’s paradox.
In the bullet item referreing to structural set theory I made “type” hyperlinked. I am wondering if at this point an explicit reference to type theory would be useful, and a comment on how it achieves something similar to the “stratification” mentioned earlier (as far as I understand).
Also maybe the Idea-section at type theory would conversely want to point to Russel’s paradox for motivation?
I could try to add some such comment, but maybe it is better you do so right away, if you have a second, instead of needing to improve on my formulation afterwards :-)
I was going to say that Russell’s paradox just doesn’t make any sense in type theory, but I guess that really is basically the same thing that happens in structural set theory. So I added a comment to that bullet point. Thanks!
Historically, there is more connection; the first explicit ‘type theory’ was Russell’s, a direct response to his paradox and the foundation used in Principia Mathematica. It’s really a sort of typed material set theory, not the type theory that we use today.
Yeah… I generally try to avoid talking about Russell’s “type theory” as much as possible, to avoid confusing people, since it’s so unlike what is nowadays called “type theory”.
Isn’t the theory of Russell types more like NF? (also relevant: this MO question of mine http://mathoverflow.net/questions/27793/russell-and-whiteheads-types-ramified-and-unramified)
I added a few remarks inspired by responses to David’s MO question.
@Toby - to the page Russell’s paradox?
Yes.
I have added some links to Bertrand Russell.
The original one page letter from the second reference is also online here.
@Nikolaj
I typeset Russell’s letter, we should probably put a clean pdf of it on the nLab.
1 to 15 of 15