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