Re: [isabelle] Existential Quantifiers

On Sun, 06 Sep 2009 20:58:06 jd at wrote:
> Hello all,
> after having thought a lot about existential quantifiers in
> predicate logic I came to the conclusion, that there is no need
> for several instances of a specific quantifier. You can
> normalize each formula to a prenex formula and afterwards
> combine the quantifiers to quantifiers over vectors.  So only
> one existential quantifier and only one all quantifier would
> suffice.

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.


Attachment: signature.asc
Description: This is a digitally signed message part.

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