FOL->ZF->HOL (Interpretation)

Hello. This may not count as a research question, but I guess it's too much for math.stackexchange.

Could we define ZF (Zermelo-Fraenkel Set theory) in classical first-order predicate calculus, then define classical HOLs(Higher order logics) so that ZF can interpret it (via "inhabits" relation (sets)) and would we get that HOLs are interpretable in FOL?

Does that mean that HOLs do not have more expressive power than FOL in principle?

-
If there is a direct method of encoding HOLs in FOL, I would be glad to see it –  Bubba88 Nov 11 '10 at 11:09
@Bubba: the simplest way is, as you say, to just interpret the higher-order quantifiers in set theory. The reason that people sometimes say that HOL has more expressive power than FOL is because they are thinking of working in the same language, just changing the allowable quantifiers. For example, the second-order theory of groups includes set quantifiers, while the first-order theory of groups does not. But the first-order theory of ZFC is expressive enough to state every sentence from the second-order theory of groups. –  Carl Mummert Nov 11 '10 at 12:41