Theory of Types

The theory of types is a logical system devised by Russell to resolve Russell's paradox by stratifying the domain of objects into a hierarchy: individuals at level 0, properties of individuals at level 1, properties of properties at level 2, and so on. A property of level n can only be predicated of objects of level n-1, making self-referential predications (such as 'the set of all sets that don't contain themselves') ill-formed rather than paradox-generating. The system was formalized in Principia Mathematica and achieved its goal of blocking the paradoxes, but at significant cost: many natural mathematical arguments require properties or classes to be predicated of objects at the same level, which the theory prohibits. Russell introduced the ramified theory of types, adding further stratifications that required the controversial Axiom of Reducibility to recover standard mathematical results. The theory of types directly influenced subsequent type systems in mathematical logic and programming language design — the type systems of languages like ML, Haskell, and Coq are descendants of Russell's original framework, stripped of its most problematic features. The Curry-Howard correspondence connects the theory of types to intuitionistic proof theory, making Russell's logical machinery the ancestor of modern functional programming.