Re: TLA+ logic

> 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.

http://us2.metamath.org:88/mpegif/mmrecent.html

> I understand that quantifying over functions is formally an “encoding” of operators in ZF, but is there an actual

> 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

will be supported by TLA).

https://en.wikipedia.org/wiki/TLA%2B

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.

http://www.sciencedirect.com/science/article/pii/S157086830700081X