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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sat, 29 May 2021 08:42:18 +0200*References*: <c52798d7-3a1f-4ebd-9025-2a1afa8b3b46n@googlegroups.com>

Hello, the implication [](\E x : F) => \EE x : []F is indeed valid. The reverse implication need not hold. For example, \EE x : []<> << x' # x >>_x is valid, but [] \E x : <> << x' # x >>_x is a contradiction. If F is a state predicate then (\EE x : []F) => [](\E x : F) is valid. Stephan
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. |

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

**References**:

- Prev by Date:
**[tlaplus] Q about the existential quantifier** - Next by Date:
**Re: [tlaplus] Curious: stuttering vs recursive** - Previous by thread:
**[tlaplus] Q about the existential quantifier** - Next by thread:
**Re: [tlaplus] Q about the existential quantifier** - Index(es):