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 a stub (in category: reference) for Principia Mathematica, in order to mention its idea of “ramified types”. Added a pointer to this to the lists of references at type theory (also at foundations of mathematics).
I’d like some kind of comment like “This is the earliest proposal of a type theory.” Or “This is the earliest substantial/formal/sensible/substantive/influential proposal…” or the like. What’s the right thing to say?
Thanks to David Roberts for highlighting this in discussion. Ultimately I’d find it fun to get a historical impression of Russell’s road from the “revolt against idealism” to type theory.
also added to Russell’s paradox – Resolutions the statement that
In Principia Mathematica Russell himself introduced a concept of ramified types in order to rule ou the paradoxical operations.
Experts please check if that’s the right way to say it.
I’m not an expert on Russell’s type theory, but that sounds about right given the little that I know of it.
I forgot, when talking with you Urs, about Simple Type Theory/Theory of Simple Types (SEP). This was what happened in between Russell and Martin-Löf. Various people worked on it, starting in the 20s, but in the hands of Church (1940) it became (maerged? Part of?) simply-typed lambda calculus (SEP).
(I’ve limited time online here in Dubai, else I would add some stuff to the lab about it)
According to the SEP: Type theory sections 2 and 3, simple type theory was introduced to block ’set of all sets which don’t contain themselves’ style paradoxes, while ramified type theory blocks liar-style paradoxes.
Thanks!
I have used that to improve and expand the beginning of the References section at type theory a little.
1 to 6 of 6