Re: [isabelle] Existential Quantifiers

This type of transformation may work in theory, but increases the length of the proof enormously. Theory again tells us that the increase in proof length could be non-elementary (inconceivably vast).
Larry Paulson

On 6 Sep 2009, at 09:58, 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. 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.