Polymorphic type checking for the type theory of the Principia Mathematica of Russell and Whitehead

Abstract
This is a brief report on results reported at length in our paper [2], made for the purpose of a presentation at the workshop to be held in November 2011 in Cambridge on the Principia Mathematica of Russell and Whitehead ([?], hereinafter referred to briefly as PM ). That paper grew out of a reading of the paper [3] of Kamareddine, Nederpelt, and Laan. We refereed this paper and found it useful for checking their examples to write our own independent computer type-checker for the type system of PM ([1]), which led us to think carefully about formalization of the language and the type system of PM A modern mathematical logician reading PM finds that it is not completely formalized in a modern sense. The type theory in particular is inarguably not formalized, as no notation for types is given at all! In PM itself, the only type annotations which appear are occasional numerical indices indicating order; the type notation we use here extends one introduced later by Ramsey. The authors of PM regard the absence of explicit indications of type as a virtue of their system: they call it “systematic ambiguity”; modern computer scientists refer to this as “polymorphism”. The language of PM is also not completely formalized, and it is typographically inconvenient for computer software to which ASCII input is to be given. The notation of PM for abstractions (propositional functions) does not use head binders; the order of the arguments of a complex expression is determined by the alphabetical order of the bound variables. For example ˆa < ˆb is the “less than” relation while ˆb < ˆa is the “greater than” relation (this is indicated by the alphabetical order of the variables). In PM , the fact that a variable is bound in a propositional function is indicated by circumflexing it. Variables bound by quantifiers are not circumflexed. A feature of the notation of [3], carried over into ours, is that no circumflexes are used: notations for propositions and the corresponding propositional functions are identical..
Keywords No keywords specified (fix it)
Categories (categorize this paper)
Options
 Save to my reading list
Follow the author(s)
Edit this record
My bibliography
Export citation
Find it on Scholar
Mark as duplicate
Request removal from index
Translate to english
Revision history
Download options
Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 30,810
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library
References found in this work BETA

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles
The Versatility of Universality inPrincipia Mathematica.Brice Halimi - 2011 - History and Philosophy of Logic 32 (3):241-264.
Types in Logic and Mathematics Before 1940.Fairouz Kamareddine, Twan Laan & Rob Nederpelt - 2002 - Bulletin of Symbolic Logic 8 (2):185-245.
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.
What is the Type-1/Type-2 Distinction?Nick Chater - 1997 - Behavioral and Brain Sciences 20 (1):68-69.
PM's Circumflex, Syntax and Philosophy of Types.Kevin C. Klement - 2013 - In Bernard Linsky & Nicholas Griffin (eds.), The Palgrave Centenary Companion to Principia Mathematica. Palgrave-Macmillan. pp. 218-246.
Added to PP index
2010-12-22

Total downloads
23 ( #226,552 of 2,202,780 )

Recent downloads (6 months)
2 ( #150,076 of 2,202,780 )

How can I increase my downloads?

Monthly downloads
My notes
Sign in to use this feature