Thanks!

I have used that to improve and expand the beginning of the References section at *type theory* a little.

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.

]]>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)

]]>I’m not an expert on Russell’s type theory, but that sounds about right given the little that I know of it.

]]>also added to *Russell’s paradox – Resolutions* the statement that

In

Principia MathematicaRussell 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.

]]>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.

]]>