Automated type-checking for the ramified theory of types of the Principia Mathematica of Russell and Whitehead

Abstract

This paper described a formal theory of type judgments for propositional logic notations of PM; I felt the need of my own automated type checker to check their examples. The type checker I wrote did indeed serve to help me referee the paper, but also took a rather different approach to notation and typing for propositional functions of PM, which proved worth writing up independently in our own paper: Holmes, M. Randall, “Polymorphic type– checking for the ramified theory of types of Principia Mathematica”, in Fairouz Kamareddine, ed., Thirty–five Years of Automating Mathematics, Kluwer, 2003, pp. 173-215.

Categories

Keywords

Reprint years

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,349

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.

My notes

Similar books and articles

Polymorphic type checking for the type theory of the Principia Mathematica of Russell and Whitehead.M. Randall Holmes - unknown
The Triumph of Types: Principia Mathematica's Impact on Computer Science.Robert L. Constable - unknown
A modern elaboration of the ramified theory of types.Twan Laan & Rob Nederpelt - 1996 - Studia Logica 57 (2-3):243 - 278.
Types in logic and mathematics before 1940.Fairouz Kamareddine, Twan Laan & Rob Nederpelt - 2002 - Bulletin of Symbolic Logic 8 (2):185-245.
The Versatility of Universality in Principia Mathematica.Brice Halimi - 2011 - History and Philosophy of Logic 32 (3):241-264.
A correspondence between Martin-löf type theory, the ramified theory of types and pure type systems.Fairouz Kamareddine & Twan Laan - 2001 - Journal of Logic, Language and Information 10 (3):375-402.
Russell's substitutional theory of classes and relations.Gregory Landini - 1987 - History and Philosophy of Logic 8 (2):171-200.
Leon Chwistek, The Principles of the Pure Type Theory , translated by Adam Trybus with an Introductory Note by Bernard Linsky.Adam Trybus - 2012 - History and Philosophy of Logic 33 (4):329-352.
Quantification Theory in *9 of Principia Mathematica.Gregory Landini - 2000 - History and Philosophy of Logic 21 (1):57-77.
Russell's divine ancestors.Dermot Cassidy - 2007 - History and Philosophy of Logic 28 (2):123-132.
Nominalization, predication and type containment.Fairouz Kamareddine & Ewan Klein - 1993 - Journal of Logic, Language and Information 2 (3):171-215.
Relations vs functions at the foundations of logic: type-theoretic considerations.Paul Oppenheimer & Edward N. Zalta - 2011 - Journal of Logic and Computation 21:351-374.
A note on Russell's paradox in locally cartesian closed categories.Andrew M. Pitts & Paul Taylor - 1989 - Studia Logica 48 (3):377 - 387.
A new interpretation of russell's multiple-relation theory of judgment.Gregory Landini - 1991 - History and Philosophy of Logic 12 (1):37-69.
First-order, Curry-typed logic for natural language semantics.Shalom Lappin - unknown

Analytics

Added to PP
2010-12-22

Downloads
46 (#336,891)

6 months
11 (#226,803)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references