ι (iota) of "individuals" from which other types are built. Russell and Whitehead's notation for building up types from other types is rather cumbersome, and the notation here is due to Church. In the ramified type theory of PM all objects are elements of various disjoint ramified types. Ramified types are implicitly built up as follows. If τ1,...,τm,σ1,...,σn are ramified types then as in simple type theory there is a type (τ1,...,τm,σ1,...,σn) of "predicative" propositional functions of τ1,...,τm,σ1,...,σn. However, there are also ramified types (τ1,...,τm|σ1,...,σn) that can be thought of as the classes of propositional functions of τ1,...τm obtained from propositional functions of type (τ1,...,τm,σ1,...,σn) by quantifying over σ1,...,σn. When n=0 (so there are no σs) these propositional functions are called predicative functions or matrices. This can be confusing because current mathematical practice does not distinguish between predicative and non-predicative functions, and in any case PM never defines exactly what a "predicative function" actually is: this is taken as a primitive notion. Russell and Whitehead found it impossible to develop mathematics while maintaining the difference between predicative and non-predicative functions, so they introduced the axiom of reducibility, saying that for every non-predicative function there is a predicative function taking the same values. In practice this axiom essentially means that the elements of type (τ1,...,τm|σ1,...,σn) can be identified with the elements of type (τ1,...,τm), which causes the hierarchy of ramified types to collapse down to simple type theory. (Strictly speaking this is not quite correct, because PM allows two propositional functions to be different even if they take the same values on all arguments; this differs from current mathematical practice where one normally identifies two such functions.) In Zermelo set theory one can model the ramified type theory of PM as follows. One picks a set ι to be the type of individuals. For example, ι might be the set of natural numbers, or the set of atoms (in a set theory with atoms) or any other set one is interested in. Then if τ1,...,τm are types, the type (τ1,...,τm) is the power set of the product τ1×...×τm, which can also be thought of informally as the set of (propositional predicative) functions from this product to a 2-element set {true,false}. The ramified type (τ1,...,τm|σ1,...,σn) can be modeled as the product of the type (τ1,...,τm,σ1,...,σn) with the set of sequences of n quantifiers (∀ or ∃) indicating which quantifier should be applied