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

# Re: [tlaplus] Q about the existential quantifier

 Hello,the implication   [](\E x : F) => \EE x : []Fis indeed valid. The reverse implication need not hold. For example,  \EE x : []<> << x' # x >>_xis valid, but  [] \E x : <> << x' # x >>_xis a contradiction. If F is a state predicate then  (\EE x : []F) => [](\E x : F)is valid.StephanOn 29 May 2021, at 05:51, ns wrote:hello, the Specifying Systems book says that a regular existentially quantified variable functions as a constant. And from the definition this does seem to be the case    \sigma |= (\E x: F) == \E x: (\sigma |= F)where \sigma is a trace. However, if I have     [] (\E x: F)its now possible for each state of \sigma to have a different value of x and satisfy this formula. But this now seems closer to a temporal existential. So would it be equivalent to     \EE x: [] F?thanks -- 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c52798d7-3a1f-4ebd-9025-2a1afa8b3b46n%40googlegroups.com. -- 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/B5C4F265-B073-42B7-B488-25BF93DC90BE%40gmail.com.

• References: