order the level of a logic as determined by the type of entity over which the free variables of that logic range. Entities of the lowest type, usually called type O, are known as individuals, and entities of higher type are constructed from entities of lower type. For example, type 1 entities are (i) functions from individuals or n-tuples of individuals to individuals, and (ii) n-place relations on individuals. First-order logic is that logic whose variables range over individuals, and a model for first-order logic includes a domain of individuals. The other logics are known as higher-order logics, and the first of these is second-order logic, in which there are variables that range over type 1 entities. In a model for second-order logic, the first-order domain determines the second-order domain. For every sentence to have a definite truth-value, only totally defined functions are allowed in the range of second-order function variables, so these variables range over the collection of total functions from n-tuples of individuals to individuals, for every value of n. The second-order predicate variables range over all subsets of n-tuples of individuals. Thus if D is the domain of individuals of a model, the type 1 entities are the union of the two sets {X: Dn: X 0 Dn$D}, {X: Dn: X 0 Dn}. Quantifiers may bind second-order variables and are subject to introduction and elimination rules. Thus whereas in first-order logic one may infer ‘Someone is wise, ‘(Dx)Wx’, from ‘Socrates is wise’, ‘Ws’, in second-order logic one may also infer ‘there is something that Socrates is’, ‘(DX)Xs’. The step from first- to second-order logic iterates: in general, type n entities are the domain of n ! 1th–order variables in n ! 1th– order logic, and the whole hierarchy is known as the theory of types. See also TYPE THEORY. G.Fo.