Re: [isabelle] Existential Quantifiers



On Tue, 2009-09-08 at 11:00 +1200, Tim McKenzie wrote:
> So you want to group all the existential quantifiers together with 
> each other, and likewise all the universal ones together?  In 
> general, ALL. EX. ALL. isn't the same as EX. ALL. ALL. or ALL. 
> ALL. EX.  For example:
> 
> ALL x. ALL y. EX z. z > x + y
> 
> is true (for various numerical types), but
> 
> ALL x. EX z. ALL y. z > x + y
> 
> is not true.

That is correct, of course.  On the other hand,

ALL x. EX z. ALL y. z(y) > x + y

*is* equivalent to the former (cf. Skolemization, axiom of choice).

Perhaps http://en.wikipedia.org/wiki/Skolem_normal_form is instructive.

Regards,
Tjark






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