Email Gateway (Aug 18 2022 at 16:50): Email Gateway (Aug 18 2022 at 16:50):From: Steve W <s.wong.731@gmail.com>
Hi again,
Firstly, thanks for advising against using axioms. I understand the danger
of axiomatisation, but deriving everything from first principles isn't my
current focus at the moment -- perhaps, I'll do that once the more urgent
stuff are sorted.
That said, are these axioms inconsistent as well?
axiomatization
S :: "real set" and
foo :: "real => real" and
bar :: "real => real" and
bax :: "real => real"
where ax1: "ALL f g. (ALL x y. x : S & y : S --> f x = g y) --> f = g"
and ax2: "ALL x y. foo (bax x) = bar (bax y)"
and ax3: "ALL x. bax x : S"
lemma "foo = bar"
using ax1 ax2 ax3
Is that the reason why the lemma can't be proved? It's ok if ax2 was "ALL x
y. foo x = bar y", satisfying the antecedent of ax1. Is something more
needed in order to prove "foo = bar"?
Thanks again
Steve
Email Gateway (Aug 18 2022 at 16:50):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
The obvious way to prove that your axioms are consistent would be to present a model of them, that is, define some S, foo, bar, bax which satisfy this property. A quick glance suggests that S=UNIV and foo=bar ought to do the trick.
Yours,
Thomas.
Email Gateway (Aug 18 2022 at 16:50):From: Brian Huffman <brianh@cs.pdx.edu>
Indeed, these axioms are consistent because it is possible to find a
model. Furthermore, you can also show that "foo = bar" is unprovable
from these axioms, since it is possible to find a model where all
axioms are satisfied, but foo is not equal to bar:
S = UNIV
foo x = x
bar x = 2 * x
bax x = 0
Email Gateway (Aug 18 2022 at 16:51):From: Stephan Merz <Stephan.Merz@loria.fr>
As others have pointed out, this set of axioms is consistent, and they don't imply your lemma. However, note that ax1 implies that S must be UNIV, and then ax1 is just equivalent to the extensionality theorem ext of HOL, and ax3 becomes trivial. (If S were different from UNIV, you could prove a contradiction by picking f and g such that they return a different result for some argument x that is not in S.)
So unless this is just something you made up for the list and that is very different from your actual work, it doesn't look like the axiomatic approach is really much easier than defining things properly. And if your axioms are more complex, the danger of introducing inconsistencies is even greater.
Stephan
Last updated: Nov 21 2024 at 12:39 UTC