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.
The interpretation of higher order logic is inherently set-theoretic, since the meaning of the second-order and higher order quantifiers depends on the set-theoretic background in which they are interpreted. Thus, in interpreting and analyzing higher order logic, we should do so in a set-theoretic context. It needn't be ZF or ZFC, but of course ZFC serves as a kind of default set-theoretic background theory for all mathematical enterprises, including the interpretation and analysis of higher order logic.
Meanwhile, there are several ways to set up the semantics for higher order logic. Considering second order logic, one can on the one hand interpret the scope of the second order quantifiers as running through all subsets of the model, or one can be explicit and insist that the model come equipped with a second-order part, an explicit family of sets that will be used for the second order quantifiers. The first method is merely an instance of the second, in which the model is equipped with the collection of all subsets. But the second method is somewhat more explicit and flexible, because it allows one to understand how the second order logic semantics are affected by various committments to which sets exist. For example, in second-order analysis, one can imagine including only arithmetically definable sets, or all hyperarithmetic sets, or projective sets, and so on, and these different second order models exhibit different second order natures.
But also, by explicitly listing the sets to be used for the second-order part, the second order logic becomes merely a multi-sorted first order logic---we now have the sets as objects in our structure. In this sense, the difference between higher order logic and first order logic disappears, and one can make the conclusion that any structure in higher order logic can be interpreted in a first order logic structure, simply by inclduing the higher order parts as actual objects.
