 Russellian types are ramified: that is, propositional functions of one and the same type belong to different orders, depending on their internal logical structures. The type of a propositional function, as we have seen, is determined by the types of its free variables. But two propositional functions φ and φ′ of the same type can involve different kinds of quantifications. If φ involves quantifications whose (bound) variables range over higher types than do the bound variables within φ′, then φ is of correspondingly higher order than φ′, even though φ and φ′ are of the same type. Recall that an impredicative propositional function φ is one that contains bound variables ranging over types as high as or higher than the type of φ itself. Assigning an impredicative propositional function to a higher order is the ramifier’s way of marking it as not kosher. 