# 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 brieﬂy 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 ﬁnds 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 circumﬂexing it. Variables bound by quantiﬁers are not circumﬂexed. A feature of the notation of [3], carried over into ours, is that no circumﬂexes 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) My bibliography Export citation Find it on Scholar Edit this record Mark as duplicate Revision history Request removal from index Translate to english

 PhilPapers Archive Upload a copy of this paper     Check publisher's policy on self-archival     Papers currently archived: 23,674 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 Only published works are available at libraries.
References found in this work BETA

No references found.

Citations of this work BETA

No citations found.

Similar books and articles

2010-12-22

21 ( #221,791 of 1,903,102 )