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

*From*: jack malkovick <sillymouse333@xxxxxxxxx>*Date*: Wed, 30 Nov 2022 02:26:25 -0800 (PST)

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)

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

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

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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4db36d5e-1661-43f3-a34c-89923ede385en%40googlegroups.com.

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

**Re: [tlaplus] simple toy theorem***From:*Stephan Merz

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

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