Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeFeb 25th 2015

    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.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeFeb 25th 2015

    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.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 26th 2015

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

    • CommentRowNumber4.
    • CommentAuthorDavidRoberts
    • CommentTimeFeb 26th 2015

    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)

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 26th 2015

    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.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeFeb 26th 2015

    Thanks!

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

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJan 23rd 2023

    added some more links, such as the ISBN:9780521067911

    diff, v6, current