[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 xcannot 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 xby 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,StephanOn 04 Dec 2015, at 14:53, Ron Pressler 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] ∈ xor even the non-TLC-supported (but perhaps TLAPS-supported?)    ∃ epsilon : ∀x : x ≠ {} ⇒ epsilon[x] ∈ xSo 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.