> So the ability to quantify over functions, plus the SUBSET and UNION operators (as well as the analogous
> INTERSECTION operator, easily defined with a set comprehension) “feel” very much second-order.
Don't forget that in ZFC a function is a class of pairs. It is possible to quantify over functions (and relations)
as long as they are not proper classes.
If you have doubt about that see Metamath.
> difference between the expressivity of TLA+ and second (and higher) -order logic?
TLAPLUS uses a formal system called temporal logic of actions (TLA). It is built over a modal logic called
linear temporal logic (ltl). Inside TLA there is a subset of ZFC (not everything expressible in ZFC
And to tell the truth I claim that second-order logic doesn't exist. All the references to it are merely allusive and
contradictory. It's just like for the Yeti. If you are looking for something of higher order that really exists,
with axioms and all what is needed, try higher-order logic.