Consider a substitutional interpretation of quantifiers with variables ranging over predicates, as in the formula, (∀P)Pa. This formula is true if and only if all of its instances are true. On a simple theory of types, the type of the variable P is &lt;i&gt;, since its arguments are all individuals (or singular terms). But the simple type of the function, (∀P)Px is also &lt;i&gt;. So an instance of (∀P)Pa is (∀P)Pa itself. A substitutional interpretation of the quantifiers requires that instances be simpler than the formulas of which they are instances. In this case, all we find out is that a particular formula is true only if it is true. This is uninformative and it seems viciously circular.