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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sun, 30 May 2021 09:13:25 -0700 (PDT)*Ironport-hdrordr*: A9a23:V19KNK6ZPbbnZ6FFdwPXwOnXdLJyesId70hD6qkmc20zTiXqraCTdZUguyMc5wx/ZJhNo7290ey7MBHhHP1Oi7X5X43SPzUO0VHAROpfBMnZsljd8kbFh4pgPMlbH5SXQbfLbGRSvILCxDj9Kc8pxLC8gdmVrNab9lNdCT5ncLth6QARMHf8LnFL*References*: <c52798d7-3a1f-4ebd-9025-2a1afa8b3b46n@googlegroups.com> <B5C4F265-B073-42B7-B488-25BF93DC90BE@gmail.com>

I misspoke: even the implication

[](\E x : F) => \EE x : []F

is not valid in general, but it is valid if F is a state predicate, or somewhat more generally, if x does not occur in the scope of temporal operators. For example, assume that v is a state variable, then

[](\E x : x = v /\ \E y : [](x=y))

is valid (it suffices at every instant to take x = v, y=x and since both x and y are rigid variables their values never change), but the formula

\EE x : [](x = v /\ \E y : [](x=y))

will not hold in general: the first conjunct requires that x and v always have the same value, but the second conjunct requires that x remains constant, which is impossible if v changes during the behavior.

For an arbitrary formula F(x), we only have

[](\E x : F(x)) => \EE x : [](\E y : y=x /\ F(y))

but this formula does not appear to be very useful.

Sincere apologies: temporal quantifiers are really delicate!

Stephan

On Saturday, May 29, 2021 at 8:42:23 AM UTC+2 Stephan Merz wrote:

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 <nedsr...@xxxxxxxxx> 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+u...@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/e67f7647-1283-4033-a9b3-f25a4ebd4b2an%40googlegroups.com.

**References**:**[tlaplus] Q about the existential quantifier***From:*ns

**Re: [tlaplus] Q about the existential quantifier***From:*Stephan Merz

- Prev by Date:
**[tlaplus] Re: How to pass a function as an argument to the other function?** - Next by Date:
**[tlaplus] Re: How to pass a function as an argument to the other function?** - Previous by thread:
**Re: [tlaplus] Q about the existential quantifier** - Next by thread:
**[tlaplus] tlc invariant violation visualization** - Index(es):