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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and