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 lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Steve W [s.wong.731 at gmail.com]
Sent: Wednesday, January 26, 2011 2:26 PM
Subject: [isabelle] Inconsistent axioms?
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"?
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