See TYPE THEORY. type theory, broadly, any theory according to which the things that exist fall into natural, perhaps mutually exclusive, categories or types. In most modern discussions, ‘type theory’ refers to the theory of logical types first sketched by Russell in The Principles of Mathematics (1903). It is a theory of logical types insofar as it purports only to classify things into the most general categories that must be presupposed by an adequate logical theory. Russell proposed his theory in response to his discovery of the now-famous paradox that bears his name. The paradox is this. Common sense suggests that some classes are members of themselves (e.g., the class of all classes), while others are not (e.g., the class of philosophers). Let R be the class whose membership consists of exactly those classes of the latter sort, i.e., those that are not members of themselves. Is R a member of itself? If so, then it is a member of the class of all classes that are not members of themselves, and hence is not a member of itself. If, on the other hand, it is not a member of itself, then it satisfies its own membership conditions, and hence is a member of itself after all. Either way there is a contradiction.
The source of the paradox, Russell suggested, is the assumption that classes and their members form a single, homogeneous logical type. To the contrary, he proposed that the logical universe is stratified into a regimented hierarchy of types. Individuals constitute the lowest type in the hierarchy, type 0. (For purposes of exposition, individuals can be taken to be ordinary objects like chairs and persons.) Type 1 consists of classes of individuals, type 2 of classes of classes of individuals, type 3 classes of classes of classes of individuals, and so on. Unlike the homogeneous universe, then, in the type hierarchy the members of a given class must all be drawn from a single logical type n, and the class itself must reside in the next higher type n ! 1. (Russell’s sketch in the Principles differs from this account in certain details.)
Russell’s paradox cannot arise in this conception of the universe of classes. Because the members of a class must all be of the same logical type, there is no such class as R, whose definition cuts across all types. Rather, there is only, for each type n, the class Rn of all non-self-membered classes of that type. Since Rn itself is of type n ! 1, the paradox breaks down: from the assumption that Rn is not a member of itself (as in fact it is not in the type hierarchy), it no longer follows that it satisfies its own membership conditions, since those conditions apply only to objects of type n.
Most formal type theories, including Russell’s own, enforce the class membership restrictions of simple type theory syntactically such that a can be asserted to be a member of b only if b is of the next higher type than a. In such theories, the definition of R, hence the paradox itself, cannot even be expressed. Numerous paradoxes remain unscathed by the simple type hierarchy. Of these, the most prominent are the semantic paradoxes, so called because they explicitly involve semantic notions like truth, as in the following version of the liar paradox. Suppose Epimenides asserts that all the propositions he asserts today are false; suppose also that that is the only proposition he asserts today. It follows immediately that, under those conditions, the proposition he asserts is true if and only if it is false. To address such paradoxes, Russell was led to the more refined and substantially more complicated system known as ramified type theory, developed in detail in his 1908 paper ‘Mathematical Logic as Based on the Theory of Types.’ In the ramified theory, propositions and properties (or propositional functions, in Russell’s jargon) come to play the central roles in the type-theoretic universe. Propositions are best construed as the metaphysical and semantical counterparts of sentences – what sentences express – and properties as the counterparts of ‘open sentences’ like ‘x is a philosopher’ that contain a variable ‘x’ in place of a noun phrase. To distinguish linguistic expressions from their semantic counterparts, the property expressed by, say, ‘x is a philosopher’, will be denoted by ‘x^ is a philosopher’, and the proposition expressed by ‘Aristotle is a philosopher’ will be denoted by ‘Aristotle is a philosopher’. A propert. . .x^ . . . is said to be true of an individual a i. . . . . . is a true proposition, and false of a i. . . . . . is a false proposition (where ‘. . . . . .’ is the result of replacing ‘x^’ with ‘a’ in ‘. . . x^ . . .’). So, e.g., x^ is a philosopher is true of Aristotle. The range of significance of a property P is the collection of objects of which P is true or false. a is a possible argument for P if it is in P’s range of significance. In the ramified theory, the hierarchy of classes is supplanted by a hierarchy of properties: first, properties of individuals (i.e., properties whose range of significance is restricted to individuals), then properties of properties of individuals, and so on. Parallel to the simple theory, then, the type of a property must exceed the type of its possible arguments by one. Thus, Russell’s paradox with R now in the guise of the property x^ is a property that is not true of itself – is avoided along analogous lines. Following the French mathematician Henri Poincaré, Russell traced the source of the semantic paradoxes to a kind of illicit self-reference. So, for example, in the liar paradox, Epimenides ostensibly asserts a proposition p about all propositions, p itself among them, namely that they are false if asserted by him today. p thus refers to itself in the sense that it – or more exactly, the sentence that expresses it – quantifies over (i.e., refers generally to all or some of the elements of) a collection of entities among which p itself is included. The source of semantic paradox thus isolated, Russell formulated the vicious circle principle (VCP), which proscribes all such self-reference in properties and propositions generally. The liar proposition p and its ilk were thus effectively banished from the realm of legitimate propositions and so the semantic paradoxes could not arise. Wedded to the restrictions of simple type theory, the VCP generates a ramified hierarchy based on a more complicated form of typing. The key notion is that of an object’s order. The order of an individual, like its type, is 0. However, the order of a property must exceed the order not only of its possible arguments, as in simple type theory, but also the orders of the things it quantifies over. Thus, type 1 properties like x^ is a philosopher and x^ is as wise as all other philosophers are first-order properties, since they are true of and, in the second instance, quantify over, individuals only. Properties like these whose order exceeds the order of their possible arguments by one are called predicative, and are of the lowest possible order relative to their range of significance. Consider, by contrast, the property (call it Q) x^ has all the (first-order) properties of a great philosopher. Like those above, Q also is a property of individuals. However, since Q quantifies over first-order properties, by the VDP, it cannot be counted among them. Accordingly, in the ramified hierarchy, Q is a second-order property of individuals, and hence non-predicative (or impredicative). Like Q, the property x^ is a (first-order) property of all great philosophers is also second-order, since its range of significance consists of objects of order 1 (and it quantifies only over objects of order 0); but since it is a property of first-order properties, it is predicative. In like manner it is possible to define third-order properties of individuals, third-order properties of first-order properties, third-order properties of second-order properties of individuals, third-order properties of secondorder properties of first-order properties, and then, in the same fashion, fourth-order properties, fifth-order properties, and so on ad infinitum. A serious shortcoming of ramified type theory, from Russell’s perspective, is that it is an inadequate foundation for classical mathematics. The most prominent difficulty is that many classical theorems appeal to definitions that, though consistent, violate the VCP. For instance, a wellknown theorem of real analysis asserts that every bounded set of real numbers has a least upper bound. In the ramified theory, real numbers are identified with certain predicative properties of rationals. Under such an identification, the usual procedure is to define the least upper bound of a bounded set S of reals to be the property (call it b) some real number in S is true of x^, and then prove that this property is itself a real number with the requisite characteristics. However, b quantifies over the real numbers. Hence, by the VCP, b cannot itself be taken to be a real number: although of the same type as the reals, and although true of the right things, b must be assigned a higher order than the reals. So, contrary to the classical theorem, S fails to have a least upper bound. Russell introduced a special axiom to obviate this difficulty: the axiom of reducibility. Reducibility says, in effect, that for any property P, there is a predicative property Q that is true of exactly the same things as P. Reducibility thus