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.
eeA:"!x. ¬(x IN emS)"
"!u. (!x. ~(x IN u)) --> u = emS"
"~(!u. (!x. ~(x IN u)) --> u = emS)"
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,
? 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and