Accordingly, Higher Order Logic (HOL) allows one to formulate claims like "Socrates has some of the properties and relations that some philosophers have". This may seem to be a minor difference with First Order Logic (FOL), but it is not, for HOL enables far more powerful logical techniques and applications than FOL.

The subject of HOL is fairly technical, interesting, and far less well-researched than FOL, since standard mathematics and logic, including set theory, are FOL theories.

The reason to prefer FOL is that it avoids quantified predicates, and therefore expressions like "for all properties", "for all functions", that were early seen as easily leading to paradoxes and unclarities.

Even so, HOL is quite close to many ordinary linguistic intuitions, since it comes easy in Natural Language to make claims about all or some properties or relations of things, and it also allows the use of elegant constructions, formulas and characterizations that cannot even be stated in FOL.

Also, varieties of HOL are known to be at least as capable as set theory, in that one can prove at least as much in it, often in more general detail or with simpler proofs, though the price is that the formal and intuitive semantics of HOL are both more difficult and less well-researched than those of FOL.

Shapiro is an interesting discussion and presentation of Second-order Logic and its advantages and setbacks; Manzano is a quite precise logical and semantical presentation of quite a few subsystems of HOL.