Re: [tlaplus] simple toy theorem

["'Martin' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

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