# 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

```

• Follow-Ups:

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