Simple contradiction proof

[jack malkovick]

I just started reading about TLAPS and I tried for fun the following silly thing

THEOREM T ==
    ASSUME
        NEW P(_),
        \A p : P(p),
        \A p : ~P(p)
    PROVE
        TRUE
    PROOF
        OBVIOUS

To my surprise, the result was green. I hoped that somehow it would "detect" the contradictions in the assumptions. 

[Stephan Merz]

Hi,

could you explain why you are surprised? The theorem holds for two reasons: (i) the assertion (TRUE) is trivial, and (ii) the assumptions are contradictory, as you say. From contradictory assumptions, anything can be proved, and in fact the following also passes:

THEOREM

    ASSUME 
        NEW P(_), 
        \A p : P(p),
        \A p : ~P(p) 
    PROVE

        FALSE
OBVIOUS

Regards,
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/904caba2-762e-49a2-bea5-1dc6a3506929n%40googlegroups.com.

[jack malkovick]

Yes, it makes sense, I tried that too before... 

I guess I was looking for a way to formulate a theorem in such a way it will be unprovable having an inconsistent set of facts.

Would that make any sense?

[Stephan Merz]

Hi,

you discovered why verification is not a panacea. You may prove the most elaborate theorems, but they are meaningless if your specification does not represent the actual system, and an inconsistent set of assumptions is just the most extreme example. Therefore, you need to be suspicious of success and validate your spec as much as you can. Simulation, as well as model checking non-properties and examining the counter-examples are useful for that.

Note that this problem applies to both model checking and theorem proving. You should get suspicious if model checking completes very quickly, finds fewer reachable states than you expect, and/or if some actions are taken only rarely or never (TLC provides statistics for this). In theorem proving, get suspicious if a proof obligation that looks complicated is solved quickly and automatically, as it may indicate a contradiction between assumptions – although this is of course not always the case.

Regards,

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a244225f-f9a0-4db7-894c-cf52fd0bd762n%40googlegroups.com.

[jack malkovick]

Thank you! You are right, being suspicious is a very healthy thing