Re: [isabelle] Proving equivalence



Actually, proving "(0::real) = 1" using that as a fact doesn't make it inconsistent, right? It just means that it has at least one unsatisfying model.

Steve

On Jan 25, 2011 9:17pm, s.wong.731 at gmail.com wrote:
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.