Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem



Here is my conclusion/lesson, which is merely stating the obvious: If I don't axiomatize things right, I get inconsistencies.

axiomatization where
  eeA:"!x. ¬(x IN emS)"

theorem emS_is_unique1:
  "!u. (!x. ~(x IN u)) --> u = emS"
  nitpick[verbose,user_axioms] oops

theorem emS_is_unique1_negation:
  "~(!u. (!x. ~(x IN u)) --> u = emS)"
  nitpick[verbose,user_axioms] oops

So nitpick finds counterexamples for both.

Unfortunately, I don't understand types, lambda calculus, and the "=" function well enough to know why.

So, I add the standard axioms, without completely understanding the underlying engine, and hope for the best. There's always the possibility that it's something embarrassingly simple.

Still, metis is pretty impressive, even though it's being applied to a simple problem. I negated emS_is_unique1 so that it started with an \<exists>, and then negated the whole thing with "~", and after defining set equality, metis proved it by the non-negated version of the theorem right above it. These things don't happen by accident, and sledgehammer is there to help make things happen.

Well, I go ahead and try to think this out. If emS_is_unique1 is false, then:

  ? u. (! x. ~(x IN u)) & (u ~= emS).

If types allow an infininite number of "u::sT" to be lurking out there, then there's a "u" distinct from emS for which I've never said that "u = emS", therefore "u ~= emS", and for which I've never used on the RHS of an "IN", therefore (!x. ~(x IN u)) .

What blows my analysis apart is that Nitpick finds a counterexample for emS_is_unique1_negation. I want to say that Nitpick shows that the negation of the theorem is true, but that would require me to ask an embarrassing question, like, "Uh, can I ask a simple question? If Nitpick finds a counterexample to a theorem, does that mean that the negation of the theorem is true?"

Things being both true and false don't make a lot of sense.
Regards,
GB





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.