 Typically these double-abstraction principles are laid down as postulates, or axioms (or axiom schemes). But that is not absolutely necessary. All that is important is whether the theory in question contains such a principle as a theorem (or theorem-scheme). Like the earlier abstraction principle for directions, HP is a double-abstraction principle. So too is Frege’s ill-fated Basic Law V, which we shall discuss in due course. 