[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Q about the existential quantifier
- From: ns <nedsri1988@xxxxxxxxx>
- Date: Fri, 28 May 2021 20:51:09 -0700 (PDT)
- Ironport-hdrordr: A9a23:4aJL4q4nynvCpYYK1gPXwNPXdLJyesId70hD6qkXc3xom62j9vxG885w6faZskdyZJhCo7690de7MBDhHPdOiOF7AV7IZmXbUQWTQb2KobGM/wHd
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
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.