# Theory of types

DOI
10.4324/9780415249126-Y030-1
DOI: 10.4324/9780415249126-Y030-1
Version: v1,  Published online: 1998
Retrieved September 21, 2020, from https://www.rep.routledge.com/articles/thematic/theory-of-types/v-1

## 1. Ramified type theory

The theory of (ramified) types was first described by Bertrand Russell (1908) as a way of avoiding vicious-circle antinomies, including the one discovered by Russell himself regarding the property that applies to all and only those properties that do not apply to themselves (see Russell, B.A.W. §§7–8; Paradoxes of set and property §5). A property is said to be ‘impredicable’ if, and only if, it is not predicable of itself; thus, the property of being impredicable is impredicable if, and only if, it is not impredicable.

From this the contradiction follows that the property of being impredicable both is and is not impredicable. The theory of ramified types for propositional functions was developed in Principia Mathematica (1910–13). For Russell, such a theory was the framework of a ‘logically perfect language’, by which he meant a language that would show at a glance the logical structure of the facts that can be described by means of it, and in particular a language ‘in which everything that we might wish to say in the way of propositions that are intelligible to us, could be said, and in which, further, structure would always be made explicit’ (1959: 165). All that would be needed to add to such a theory is a vocabulary of descriptive constants that correspond to the meaningful words and phrases of the natural sciences or of natural language. The basic laws of a natural science would then be listed as nonlogical postulates of that science, and (as later proposed by Rudolf Carnap) the analytic connections between the words and phrases of natural language would be listed as meaning postulates. The constants and postulates of pure mathematics do not also need to be added, according to Russell, because they are all definable and provable in purely logical terms within the framework of type theory itself – a view known as (Russell’s form of) logicism (see Logicism §1).

The way type theory avoids vicious-circle antinomies is by imposing logico-grammatical constraints on the logic of predicates. The basic idea is that predicates (and the propositional functions they stand for) are to be typed in a hierarchical manner so that predicates of a given type (and their corresponding propositional functions) could never meaningfully be applied to predicates (propositional functions) of the same or higher type. (Thus both Impred(Impred) and ¬Impred(Impred) are meaningless in type theory.) In ‘ramified’ type theory, the hierarchy is, as it were, two-dimensional, having a ‘vertical’ dimension consisting of a hierarchy of orders and, within each order, a ‘horizontal’ dimension consisting of a hierarchy of levels. That is, properties are distinguished in ramified type theory as being both of a given order (for example, first-order, second-order and so on) and of a specific level within that order. Thus, for example, where ‘being shrewd’, ‘being courageous’, ‘being insightful about enemy positions’ and so on are examples of first-order/first-level properties that Napoleon and other great generals shared (that is, properties of r-type (i)/1, as defined below, assuming Napoleon and other generals to be of r-type i), Napoleon’s having all of the (first-order/first-level) properties of a great general – that is, all of the (first-order/first-level) properties that make up what it is to be a great general – amounts to Napoleon having a first-order property of level two (that is, a property of r-type (i)/2, as defined below). ‘Simple’ type theory has only the ‘vertical’ hierarchy.

The description of the ramified hierarchy given by Russell was informal and relied on a use/mention confusion (see Use/mention distinction and quotation §3) between propositional functions (properties or relations) and the open formulas with ‘apparent’ (that is, ‘bound’ as opposed to ‘free’) variables taken to represent those functions. The ramified theory was not given a precise, formal description until Alonzo Church’s paper of 1976, which, in accordance with contemporary terminology, uses the notion of ‘order’ to represent the ‘vertical’ hierarchy (instead of Russell’s informal notion of order corresponding to the ‘horizontal’ hierarchy), and which uses the notion of ‘level’ to represent the ‘horizontal’ hierarchy. Church’s definition of ramified types (‘r-types’) is as follows:

1. There is an r-type i to which all and only individuals belong, and whose order is stipulated to be 0.

2. If m is a non-negative integer and n is a positive integer and β1,…, βm are any given r-types, then there is an r-type (β1,…, βm)/n to which belong all and only m-ary propositional functions of level n and with arguments of r-types ≤β1,…,βm, respectively; and the order of such a function is N+n, where N is the greatest of the orders corresponding to the types β1,…,βm (and N=0 if m=0).

Here, by an ‘individual’, that is, an entity of r-type i, Russell meant a concrete object (in particular, an event) as compared to the propositional functions (abstract properties and relations) that make up the entities of all other r-types. (It is not essential for all logical purposes that the entities of the basic type i be concrete, however.) The notion of the level of a propositional function φ of r-type (β1,…,βm)/n represents what Russell intended in speaking informally of the ‘apparent’ (bound) variables occurring in φ. If N, for example, is the greatest of the orders of β1,…,βm, and k is the greatest of the orders of the ‘apparent’ variables occurring in φ (construed as a formula of r-type (β1,…,βm)/n), then n=1 if k≤N, and n=k+1 if N<k. According to Russell, a propositional function (or formula for such) was said to be ‘predicative’ if ‘it is of the lowest order compatible with its having the arguments it has’ (1910–13: vol. 1, 53); that is, in terms of the notion of level, φ is predicative if, and only if, n=1.

In the simple theory of types the distinction between levels is dropped and only the distinction between orders is retained, so that in effect all propositional functions of the simple theory are predicative – although the comprehension principle of simple type theory, unlike that of ramified type theory, allows that such functions can be specified ‘impredicatively’, that is, in terms of a totality to which they belong.