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