MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

## 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 2010 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 2010 at 12:41

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.

-
The key point is that, when discussing higher order logic, we have to be very explicit about the semantics that we want to use. There is nothing syntactic about higher-order logic that cannot be done with first-order logic, but full higher-order semantics are much stronger than first-order (Henkin) semantics. – Carl Mummert Nov 11 2010 at 12:27
Also, although I (as a mathematical logician) am fine with simply viewing full higher-order semantics as being defined relative to a model of set theory, and thus really a sort of first-order semantics that incorporates set theory, that is only one way of looking at it. A logician of a less mathematical nature might simply view the semantics as being disquotational, for example. The distinction here is somewhat philosophical, but it's worth pointing out that not everyone would agree with our set-theory-reductionist viewpoint. – Carl Mummert Nov 11 2010 at 12:33
Thanks, Carl, I agree with your comments. – Joel David Hamkins Nov 11 2010 at 13:07
I would be one of those logicians who disagree with set-theory-reductionist viewpoint. Higher-order logic can have many other interpretations (toposes come to mind). – Andrej Bauer Nov 11 2010 at 14:18
@Andrej: Thanks for pointing out that gaping omission in my comment. Certainly there are also many mathematical logicians who wouldn't favor viewing HOL as just a jargon for set theory; I was not intending to leave them out. – Carl Mummert Nov 11 2010 at 14:45