Re: [isabelle] Inconsistent axioms?

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.


From: cl-isabelle-users-bounces at [cl-isabelle-users-bounces at] On Behalf Of Steve W [s.wong.731 at]
Sent: Wednesday, January 26, 2011 2:26 PM
To: isabelle-users
Subject: [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


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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