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

Re: [tlaplus] TLA+ logic



Ron,

the logic of TLA+ is a first-order logic because you cannot quantify over operators, as in

  \E Op : \A x : Op(x) # x

(However, note that operator definitions in TLA+ can have operator arguments.)

The fact that in set theory, sets (and functions) are ordinary values and so one may quantify over them is confusing at first. As you say, the language "feels" second-order. Formally, it is not because the interpretation of "\in" is only fixed up to the (Zermelo-Fraenkel) axioms.

You may want to look at http://math.stackexchange.com/questions/23799/first-order-logic-vs-second-order-logic and similar references for more in-depth discussions of this.

Concerning your concrete example,

  \E epsilon : \A x : x # {} => epsilon[x] \in x

cannot be proved because the function would have to be "too big" to be a set (its domain would have to contain all values, which is not a set but a class). However, it is easy to prove

  \A S : S # {} => \E epsilon \in [SUBSET S -> S] : \A x \in SUBSET S : x # {} => epsilon[x] \in x

by defining the witness

  eps == [T \in SUBSET S |-> IF T = {} THEN CHOOSE x \in S : TRUE
                                       ELSE CHOOSE x \in T : TRUE]

(The "THEN" branch is necessary to ensure eps \in [SUBSET S -> S].)

Regards,
Stephan


On 04 Dec 2015, at 14:53, Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx> wrote:

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


--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.