[isabelle] Inconsistent axioms?

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?

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


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