Re: [isabelle] Proving equivalence


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


On Jan 25, 2011 6:11pm, Brian Huffman <brianh at> 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


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