Higher Order Logic: In
logic: Systems of Predicate Logic that
allow quantification of both predicates
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.