# Re: [tlaplus] Rigid and flexible variables

> On 27 Nov 2016, at 19:09, 'fl' via tlaplus <tla...@xxxxxxxxxxxxxxxx> wrote:
>
>
> I've just read Leslie Lamport's "Temporal Logic of Actions" ACM Transactions on Programming Languages and Systems, 1994:
>
> http://dl.acm.org/citation.cfm?id=177726
>
> http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-actions.pdf
>
>

The TOPLAS paper describes the temporal logic TLA, whereas the specification language TLA+, supported by TLC and TLAPS, combines (Zermelo-Fraenkel) set theory for data structures and TLA for specifying behavior.

> And I just wonder: when in a proof the goal is:
>
>    \A x \in A : P (A a set, P an action),
>
> and then you have the step:
>
>    TAKE x \in A,
>
> what is the status of x?
>
> I bet for a rigid variable (see p. 6). (The other possibility would be a variable neither rigid nor flexible but I don't think so.)

Yes, variables introduced by TAKE are rigid. TLAPS has no support so far for the quantifiers \AA and \EE.

Best regards,

Stephan



• Follow-Ups: