 The doctrine of types is based upon the observation that universal quantification—understood as full generality, i.e., when \(x\) ranges ‘over the whole universe’—does not make sense: when we state that \(\forall x\phi(x)\) is true, we only claim the function \(\phi(x)\) has the value ‘true’ for all arguments \(x\) for which it is meaningful. The essential point is that each propositional function has a range of significance, i.e., a type, and quantification is legitimate only over types. Formally speaking, each variable must have a preassigned type. The paradoxes (or reflexive fallacies) prove that certain collections, such as the totality of all propositions, of all classes and so on, cannot be types. So we can quantify over the collection of men, but we cannot properly state ‘all propositions of the form \(p\vee \neg p\) are true’. Therefore, the logical entities divide into types, and, in particular, every propositional function must have a higher type than its arguments. Moreover, in the light of the vicious circle principle, the notion of order must also be introduced. No object can be defined by quantifying over a totality which contains the object itself as element; hence the order of every propositional function must be greater than the order of propositional functions over which it quantifies.