[isabelle] Existential Quantifiers

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. Am I right? a) If yes, can you tell a method for 
decomposition of vectorized quantifiers? b) If not, please give an 
example, where vectorization does not work.

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