 Russell’s discovery in 1901 of the Russell Paradox led him within a few months, in a letter to Frege (Frege [PMC]: 144) to propose a tentative version of the theory of types. The central idea he took from Frege’s theory of functions of the first, second, and higher orders. Russell presented a version of his theory in an appendix to the Principles of Mathematics (1903), and then in a mature form in his “Mathematical Logic as Based on the Theory of Types” (1908), which provided the conceptual underpinnings for Principia Mathematica. Russell views the universe as striated into levels or types. The first type comprises the individuals; the second type comprises the “first-order” propositions whose quantifiers range over the individuals of the first type; in general, the quantifiers in propositions of the n+1st type range over propositions of the nth type. Russell’s system in fact comprises two distinct hierarchies: one to deal with the paradoxes of set theory (specifically, to prohibit sets from being elements of themselves); the other to deal with the semantical paradoxes (such as the paradox of the liar). This dual structure, branching in two directions, gives his theory the name “ramified theory of types”. In order to be able to establish classical analysis, he was forced to adopt the axiom of reducibility, which provides that any function of level \(n+1\) is coextensive with a predicate of function of lower level. The system was immensely complicated; in time, at the hands of Chwistek, Ramsey, Carnap, Tarski, and Church, it was recognized that the hierarchy dealing with the semantical paradoxes could be pruned away, leaving the “simple theory of types”. (A survey of this evolution can be found in Church 1974, and detailed examinations of Russell’s theory in Landini 1998 and Linsky 2011.)