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

nLab > Latest Changes: Principia Mathematica

Bottom of Page

1 to 7 of 7

  1.  
    • 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

1 to 7 of 7

  1.