Re: [isabelle] Proving equivalence



On Tue, Jan 25, 2011 at 1:17 PM,  <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?

Start with your axiom:

ax1: "ALL p r v e. (r = foo p e & v = bar p e) = (bax r e = v)"

Now instantiate "v" to "bax r e":

"ALL p r e. (r = foo p e & bax r e = bar p e) = (bax r e = bax r e)"

Simplify:

"ALL p r e. (r = foo p e & bax r e = bar p e) = True"
"ALL p r e. r = foo p e & bax r e = bar p e"

Take the first conjunct:

"ALL p r e. r = foo p e"

This states that all real numbers "r" are equal to the same value "foo
p e", which is obviously inconsistent.

- Brian





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