 Finally, our type-theory, intensional or extensional, is higher-order, because the semantics makes available higher-order domains of quantification and reference. sweater refers to a property of individuals, a first-order property. (every(sweater)) refers to a property of properties of individuals, a second-order property. For just as sweater(my favorite garment) attributes the property of being a sweater to a certain individual, so we can think of (every(sweater))(woollen) as attributing a property to the property of being woollen. Which property is attributed to being woollen? The rules governing every ensure that (every(F)) is truly predicated of G iff G is a property of every F. In that case, G has the property of being a property of every F. So (every(F)) stands for the property of being a property of every F.