Email Gateway (Aug 18 2022 at 16:49): Email Gateway (Aug 18 2022 at 16:49):From: Steve W <s.wong.731@gmail.com>
Hi all,
I'm having problem proving the following. Say I have:
axiomatization
foo :: "real => real => real" and
bar :: "real => real => real" and
bax :: "real => real => real"
where ax1: "ALL p r v e. (r = foo p e & v = bar p e) = (bax r e = v)"
lemma "ALL p r v e. bax r e = bar p e"
using ax1
by auto
The lemma can be proved. However, if I change the signature of bax to "real
=> real => real => real":
axiomatization
foo :: "real => real => real" and
bar :: "real => real => real" and
bax :: "real => real => real => real"
where ax2: "ALL q p r v e. (r = foo p e & v = bar p e) = (bax q r e = v)"
lemma "ALL q p r v e. bax q r e = bar p e"
using ax2
by auto
Auto can't find a proof. How come this is so difficult for auto? What is the
proper way to do this proof?
Thanks
Steve
Email Gateway (Aug 18 2022 at 16:49):From: Tjark Weber <webertj@in.tum.de>
Steve,
both "by blast" and "by metis" succeed. I didn't investigate why auto
fails.
Kind regards,
Tjark
Email Gateway (Aug 18 2022 at 16:50):From: Brian Huffman <brianh@cs.pdx.edu>
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!
Email Gateway (Aug 18 2022 at 16:50):From: s.wong.731@gmail.com
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
Email Gateway (Aug 18 2022 at 16:50):From: s.wong.731@gmail.com
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
Email Gateway (Aug 18 2022 at 16:50):From: Brian Huffman <brianh@cs.pdx.edu>
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.
Email Gateway (Aug 18 2022 at 16:50):From: Brian Huffman <brianh@cs.pdx.edu>
If "False" can be derived as a theorem from some set of axioms, then
any proposition can be derived as a theorem, and so by definition that
set of axioms is inconsistent.
Note that my proof of "(0::real) = 1" from ax1 did not rely on any
extra assumptions about the constants "foo", "bar", etc. so the proof
applies to all potential models.
Last updated: Nov 21 2024 at 12:39 UTC