Re: [isabelle] Inconsistent axioms?



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

On 26 Jan 2011, at 04:26, Steve W wrote:

> 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






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