To block this sort of circularity, we can turn to the ramified theory of types. On the ramified theory, the propositional function (∀P)Px is of order 2, because of the presence of the quantifier binding a variable of order 1. In this way, the ramified theory forces formulas to be simpler (at least in terms of order) than the formulas of which they are instances (see Hazen and Davoren 2000).