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

*From*: "'Martin' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Wed, 30 Nov 2022 12:20:21 +0100*References*: <4db36d5e-1661-43f3-a34c-89923ede385en@googlegroups.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:102.0) Gecko/20100101 Thunderbird/102.5.0

I stripped your proof down to: THEOREM T == ASSUME NEW S(_), NEW U(_), NEW M(_), NEW P(_), NEW B(_), \A x : U(x), \A x : ~U(x) PROVE FALSE PROOF OBVIOUS

cheers, Martin On 11/30/22 11:26, jack malkovick wrote:

Let's say we have this simple theorem THEOREM T == ASSUME NEW NEW S(_), NEW U(_), NEW M(_), NEW P(_), \A x : M(x) = S(x) /\ ~U(x), \A x : P(x) = M(x) PROVE \A x : P(x) => S(x) PROOF OBVIOUS It is true.If I negate the goal to \E x : ~(P(x) => S(x)) same as \E x : P(x) /\ ~S(x) itbecomes red.However, if I add another assumption NEW B(_), \A x : B(x) = S(x) /\ U(x), The theorem turns green! How can this new assumption make the theorem true? --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 emailto tlaplus+unsubscribe@xxxxxxxxxxxxxxxx<mailto:tlaplus+unsubscribe@xxxxxxxxxxxxxxxx>.To view this discussion on the web visithttps://groups.google.com/d/msgid/tlaplus/4db36d5e-1661-43f3-a34c-89923ede385en%40googlegroups.com <https://groups.google.com/d/msgid/tlaplus/4db36d5e-1661-43f3-a34c-89923ede385en%40googlegroups.com?utm_medium=email&utm_source=footer>.

-- 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/cb8d181a-2693-a33e-f29b-616b84003534%40gmail.com.

**Follow-Ups**:**Re: [tlaplus] simple toy theorem***From:*jack malkovick

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

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