FOM: First-order logic -- a query

[JSHIPMAN@bloomberg.net]

Kanovei reminds us that set theory is the "official" foundation for
mathematical *objects* and "classical mathematical logic" is the foundation for
mathematical *reasoning*.  But what exactly is "classical mathematical logic"?
In my view it is primarily the first-order predicate calculus of Frege which
*when used with set theory* suffices to develop everything.  If you don't have
the axioms of power set and comprehension and don't like to use sets you need a
higher-order logic or a type theory.  My question is "what is gained by this"?
It seems that the most serious objections to using a set theory along with
first-order logic are the existence of non-standard models and the ontological
fuzziness of the levels of the hierarchy past Vomega+omega, but the benefits
(completeness theorems, transfinite induction, simplicity, logical strength, the
ability to even contemplate levels like Vomega+omega) look much weightier.
After all, if your ultimate aim is to establish theorems of "ordinary
mathematics" you don't care about nonstandard models or (usually) higher levels.
So why would one use higher-order logic instead of Z or ZF or ZFC? - Joe Shipman