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 FOL doesn't have more expressive power than HOLs in principle?

Thank you in advance.

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?

Thank you in advance.