 Now ‘type’ is a very overworked word. Tokens of that type, to use one of its meanings (roughly as abstract syntactic object), have sometimes been used to stand for properties, including higher-order properties, as in Russell’s various type theories. Church was to continue this tradition in his simple typed version of \(\lambda\)-calculus (Church, 1940). In this usage, types, such as the property of caninity or of being a shape, have instances such as Fido, in the first case, or the lower-order property of being square in the second case. Thus instances of types in this sense need not be abstract entities. Another usage is syntactic, as when the basic expressions of a language are divided into various disjoint categories (‘types’) and formation rules for generating well-formed expressions are set down making use of the type distinctions. In this usage ‘type’ is an expression in the syntactic metatheory of the language of some object theory. In some cases the syntactic theory is in fact part of the object theory under discussion. Independently of this, some presentations of syntactic type theories ‘push down’ the syntactic metatheory into the object theory under discussion by stipulating that the well-formed expressions of the object language contain syntactic proper parts, tags as it were, which are correlated with the metatheoretic type of the expression and have no semantic role. In Howard (1969), for example, the well-formed formula of the conditional fragment of propositional logic are used as type symbols superscripting terms of the type theory. 