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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 30 Nov 2022 11:44:53 +0100*References*: <4db36d5e-1661-43f3-a34c-89923ede385en@googlegroups.com>

I think this is a matter of parsing precedence. \A x : M(x) = S(x) /\ ~U(x) is parsed as \A x : (M(x) = S(x)) /\ ~U(x) and therefore your hypotheses imply \A x : ~ U(x) For the analogous reason, the hypothesis NEW B(_), \A x : B(x) = S(x) /\ U(x) asserts \A x : U(x) and now you get an inconsistent set of assumptions. Had you used "<=>" instead of "=", the result would have been different because conjunction binds more tightly than equivalence. 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/81603491-C40C-4B21-854F-71FE85158AE9%40gmail.com. |

**References**:**[tlaplus] simple toy theorem***From:*jack malkovick

- Prev by Date:
**[tlaplus] Re: simple toy theorem** - Next by Date:
**Re: [tlaplus] simple toy theorem** - Previous by thread:
**[tlaplus] Re: simple toy theorem** - Next by thread:
**Re: [tlaplus] simple toy theorem** - Index(es):