Re: [isabelle] A proof for existential

On Wed, Aug 4, 2010 at 8:41 AM, Thomas Sewell
<Thomas.Sewell at> wrote:
> There is a parse problem with your axioms ax1 and ax2. I am assuming that by => you mean the operator --> which is the implication operator of HOL.

Indeed. Apologies for the typo.

> If so, the problem is that your goal is false. The real problem is that your second axiom is a truism. It says there exists an x which is a zero of g if it is a strict maximum of h. In fact there always exist infinitely many x which satisfy this property - they may not be zeroes of g, but they are not the strict maximum of h.

I'm a bit confused: If ax2 is a truism, why is the goal false? To
prove the goal, wouldn't I need to show that there exists some x which
is a strict maximum of h (ax1)?


> Yours,
>    Thomas.
> ________________________________________
> From: cl-isabelle-users-bounces at [cl-isabelle-users-bounces at] On Behalf Of munddr at [munddr at]
> Sent: Wednesday, August 04, 2010 4:29 AM
> To: isabelle-users at
> Subject: [isabelle] A proof for existential
> Hi all,
> I've been stuck trying to find a proof for the following, could someone
> please shed some light?
> axiomatization
> f :: "real => real" and
> g :: "real => real" and
> h :: "real => real" where
> ax1: "EX x. ALL y. x ~= y => hx > h y" and
> ax2 :"EX x. (ALL y. x ~= y => hx > hy) => gx = 0"
> lemma "EX x. gx = 0"
> oops
> I've tried:
> lemma "EX x. gx = 0"
> using ax1 ax2
> apply (intro exI)
> apply (erule exE)+
> apply (erule allE)
> apply (erule impE)
> which gives 2 subgoals, but they don't seem to be in the right direction...
> Thanks for the help in advance.
> Thanks
> John
> 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.