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 | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,679 |
| External links |
  Try with proxy. |
| Through your library | Only published papers are available at libraries |
Similar books and articlesTwan Laan & Rob Nederpelt (1996). A Modern Elaboration of the Ramified Theory of Types. Studia Logica 57 (2-3):243 - 278.
Fairouz Kamareddine & Twan Laan (2001). A Correspondence Between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems. Journal of Logic, Language and Information 10 (3):375-402.
Brice Halimi (2011). The Versatility of Universality inPrincipia Mathematica. History and Philosophy of Logic 32 (3):241-264.
Fairouz Kamareddine, Twan Laan & Rob Nederpelt (2002). Types in Logic and Mathematics Before 1940. Bulletin of Symbolic Logic 8 (2):185-245.
Adam Trybus (2012). Leon Chwistek, The Principles of the Pure Type Theory (1922), Translated by Adam Trybus with an Introductory Note by Bernard Linsky. History and Philosophy of Logic 33 (4):329-352.
Dermot Cassidy (2007). Russell's Divine Ancestors. History and Philosophy of Logic 28 (2):123-132.
Fairouz Kamareddine & Ewan Klein (1993). Nominalization, Predication and Type Containment. Journal of Logic, Language and Information 2 (3):171-215.
Nick Chater (1997). What is the Type-1/Type-2 Distinction? Behavioral and Brain Sciences 20 (1):68-69.
Kevin C. Klement (forthcoming). PM's Circumflex, Syntax and Philosophy of Types. In Bernard Linsky & Nicholas Griffin (eds.), Principia Mathematica at 100. Cambridge.
Analytics
Monthly downloads |
Added to index2010-12-22Total downloads4 ( #178,675 of 549,078 )Recent downloads (6 months)1 ( #63,317 of 549,078 )How can I increase my downloads? |
My notes
Discussion
