One reason to take the ramified theory of types seriously (even without accepting propositions) is that it can be usefully incorporated into a substitutional theory of quantification. On the substitutional interpretation of the quantifiers, a universally quantified formula such as (∀x)Fx is true if and only if all of its instances Fa1, Fa2, Fa3,… are true. Similarly, (∀x)Fa is true if and only if at least one of its instances is true. 