A modern elaboration of the ramified theory of types

The paper first formalizes the ramified type theory as (informally) described in the Principia Mathematica 32]. This formalization is close to the ideas of the Principia, but also meets contemporary requirements on formality and accuracy, and therefore is a new supply to the known literature on the Principia (like 25], 19], 6] and 7]).As an alternative, notions from the ramified type theory are expressed in a lambda calculus style. This situates the type system of Russell and Whitehead in a modern setting. Both formalizations are inspired by current developments in research on type theory and typed lambda calculus; see 3].Supported by the Co-operation Centre Tilburg and Eindhoven Universities. ¹32], Introduction, Chapter II, Section I, p. 37.Presented by Wolfgang Rautenberg