I've seen it mentioned (both by Leslie Lamport and Stephan Merz) that TLA+ is a first order logic. However, it is trivial to write expressions like:
∃ epsilon ∈ [SUBSET S → S] : ∀x ∈ SUBSET S : x ≠ {} ⇒ epsilon[x] ∈ x
or even the non-TLC-supported (but perhaps TLAPS-supported?)
∃ epsilon : ∀x : x ≠ {} ⇒ epsilon[x] ∈ x
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. 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?
Ron