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

*From*: jack malkovick <sillymouse333@xxxxxxxxx>*Date*: Wed, 30 Nov 2022 04:15:26 -0800 (PST)*References*: <4db36d5e-1661-43f3-a34c-89923ede385en@googlegroups.com> <cb8d181a-2693-a33e-f29b-616b84003534@gmail.com>

Thank you all for the clear explanation

On Wednesday, November 30, 2022 at 1:20:28 PM UTC+2 martin...@xxxxxxxxxxxxxx wrote:

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

The equality binds stronger than the conjunction, such that the axiom is

parenthesized as \A x : (M(x) = S(x)) /\ ~U(x) allowing me to remove the other

conjunct from the universal quantification. Now it's easily visible that the

assumptions are a contradiction :)

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) it

> becomes 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 email

> to tlaplus+u...@xxxxxxxxxxxxxxxx

> <mailto:tlaplus+u...@xxxxxxxxxxxxxxxx>.

> To view this discussion on the web visit

> https://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/b19451eb-e6b8-4014-a7e1-e78090c284f6n%40googlegroups.com.

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

**Re: [tlaplus] simple toy theorem***From:*'Martin' via tlaplus

- Prev by Date:
**Re: [tlaplus] simple toy theorem** - Next by Date:
**[tlaplus] How can I define a sequence as part of a record's fields?** - Previous by thread:
**Re: [tlaplus] simple toy theorem** - Next by thread:
**[tlaplus] How can I define a sequence as part of a record's fields?** - Index(es):