Theory of Types

In 1902, Russell discovered a contradiction in Frege's logical system. Consider the set R of all sets that do not contain themselves as members. If R contains itself, then by definition it must not contain itself; if R does not contain itself, then by definition it must contain itself. Either way, a contradiction follows. The paradox is not a curiosity but a fundamental problem for any theory that freely forms sets from predicates — which is to say, for any theory that hopes to derive mathematics from logic in the Fregean way.

The theory of types resolves the paradox by ruling that every entity belongs to a determinate logical type, and that expressions of one type cannot be meaningfully predicated of entities of a different type. Individuals are type 0; propositional functions that apply to individuals are type 1; propositional functions that apply to type-1 functions are type 2; and so on. A set can only have members of a lower type than itself — which means the self-referential construction "the set of all sets" is not just false but syntactically ill-formed. The paradox dissolves because R cannot be meaningfully said to contain or fail to contain itself.

The ramified version of the theory, required to block more subtle paradoxes, introduces a further stratification within each type — distinguishing predicative and non-predicative functions — that creates significant technical problems for the derivation of mathematics. To recover what is needed, Russell and Whitehead introduce the Axiom of Reducibility: for every non-predicative function, there is a coextensive predicative function. This axiom was widely regarded as philosophically ad hoc — it is not a logical truth in any obvious sense — and became one of the main points of criticism of the Principia programme. Ramsey and others subsequently proposed simplifications that dispensed with it.

Russell first articulated the simple theory of types in "Mathematical Logic as Based on the Theory of Types" (1908). The ramified version in Principia Mathematica was later simplified by Ramsey's simple type theory, which dropped the intra-type stratification and the Axiom of Reducibility.