Re: [tlaplus] Simple contradiction proof

On Wednesday, November 30, 2022 at 12:04:50 PM UTC+2 Stephan Merz wrote:

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

On 30 Nov 2022, at 10:11, jack malkovick <sillym...@xxxxxxxxx> wrote:

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?

On Wednesday, November 30, 2022 at 11:04:37 AM UTC+2 Stephan Merz wrote:
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

On 30 Nov 2022, at 09:53, jack malkovick <sillym...@xxxxxxxxx> wrote:

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.

--
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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/904caba2-762e-49a2-bea5-1dc6a3506929n%40googlegroups.com.

--
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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a244225f-f9a0-4db7-894c-cf52fd0bd762n%40googlegroups.com.