# Re: [isabelle] Proving equivalence

```Hi,

```
Thanks for pointing out the inconsistency. Just curious, how could you could spot the inconsistency? How could "(0::real) = 1" be derived from that axiom?
```
Thanks again

Steve

On Jan 25, 2011 6:11pm, Brian Huffman <brianh at cs.pdx.edu> wrote:
```
```Hi Steve,
```
```

```
```As Tjark pointed out recently, axioms are evil. It just so happens
```
```
```
```that both of your example axiomatizations are inconsistent. As you can
```
```
```
```see:
```
```

```
```lemma "(0::real) = 1"
```
```
```
```using ax1 by metis
```
```

```
```(The same proof works also for ax2.)
```
```

```
```This might explain why metis can easily solve your lemma: because from
```
```
```
```ax1 or ax2 metis can prove any equation between real numbers!
```
```

```
```- Brian
```
```

```
```On Tue, Jan 25, 2011 at 9:18 AM, Tjark Weber webertj at in.tum.de> wrote:
```
```
```
```> Steve,
```
```
```
```>
```
```
```
```> On Tue, 2011-01-25 at 16:51 +0000, Steve W wrote:
```
```
```
```>> Auto can't find a proof. How come this is so difficult for auto? What
```
```
```
```>> is the proper way to do this proof?
```
```
```
```>
```
```
```
```> both "by blast" and "by metis" succeed. I didn't investigate why auto
```
```
```
```> fails.
```
```
```
```>
```
```
```
```> Kind regards,
```
```
```
```> Tjark
```
```
```
```>
```
```
```
```>
```
```
```
```>
```
```

```

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