# Re: [isabelle] A proof for existential

Dear John,
On Tue, 2010-08-03 at 18:29 +0000, munddr at gmail.com 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 ...
Regards,
Tjark

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