simple toy theorem

[jack malkovick]

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?

[jack malkovick]

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

[Stephan Merz]

I think this is a matter of parsing precedence.

  \A x : M(x) = S(x) /\ ~U(x)

is parsed as

  \A x : (M(x) = S(x)) /\ ~U(x)

and therefore your hypotheses imply

   \A x : ~ U(x)

For the analogous reason, the hypothesis

  NEW B(_), \A x : B(x) = S(x) /\ U(x)

asserts

  \A x : U(x)

and now you get an inconsistent set of assumptions. Had you used "<=>" instead of "=", the result would have been different because conjunction binds more tightly than equivalence.

Stephan

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4db36d5e-1661-43f3-a34c-89923ede385en%40googlegroups.com.

[Martin]

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

> --
> 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...@googlegroups.com

> <mailto:tlaplus+u...@googlegroups.com>.

> 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>.

[jack malkovick]

Thank you all for the clear explanation