[tlaplus] Re: simple toy theorem

[jack malkovick <sillymouse333@xxxxxxxxx>]

Did this new assumption introduced an inconsistency? I don't see how, but I miss something for sure...

On Wednesday, November 30, 2022 at 12:26:26 PM UTC+2 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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d0896133-b1b7-4bce-9d53-575d4f9f52afn%40googlegroups.com.