Re: [isabelle] A proof for existential

Dear John,

On Tue, 2010-08-03 at 18:29 +0000, munddr at wrote:
> 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"

Your formalization contains a few typos.  Note that you need a space
between functions and their arguments, e.g. "h x" instead of "hx".
Also, => denotes function types, but implication must be written -->.

> lemma "EX x. gx = 0"
> oops

The lemma doesn't follow from ax1 and ax2.  ax1 says that h has a strict
global maximum.  ax2 says that there is an x such that if x is a strict
global maximum of h, then x is a root of g.  (Note that the scope of the
existential quantifier extends all the way to the end of the formula.)

ax2 is actually a theorem (for any functions h and g, regardless of
ax1).  Proof: simply choose some x that is *not* a strict global maximum
of h, then the implication becomes vacuously true.

So you're trying to show that g has a root, provided that h has a strict
global maximum.  Well, it's no surprise you can't find a proof ...


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