Polymorphic type-checking for the ramified theory of types of Principia Mathematica

AbstractA formal presentation of the ramified theory of types of the Principia Mathematica of Russell and Whitehead is given. The treatment is inspired by but differs sharply from that in a recent paper of Kamareddine, Nederpelt and Laan. A complete algorithm for determining typability and most general polymorphic types of propositional functions of the ramified theory of types is presented, unusual in requiring reasoning about numerical inequalities in the course of deduction of type judgments (to support unification of orders). Software implementing these algorithms has been developed by the author, and examples of the use of the software are presented. This is an abridged version of a longer paper which may appear later elsewhere