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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Fri, 4 Dec 2015 05:53:41 -0800 (PST)

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

**Follow-Ups**:**Re: [tlaplus] TLA+ logic***From:*Stephan Merz

**Re: TLA+ logic***From:*fl

- Prev by Date:
**Re: [tlaplus] The effect of symmetry sets on TLC performance** - Next by Date:
**Re: TLA+ logic** - Previous by thread:
**Re: [tlaplus] TLA+ Toolbox nightly: Periodic workspace save java.lang.NumberFormatException** - Next by thread:
**Re: TLA+ logic** - Index(es):