Re: [isabelle] Inconsistent axioms?



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

- Brian

On Tue, Jan 25, 2011 at 7:40 PM, Thomas Sewell
<Thomas.Sewell at nicta.com.au> wrote:
> 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.
>
> ________________________________________
> 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
> 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?
>
> 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
>
> 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.