[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

TLA+ logic

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?