[isabelle-dev] not-exists problem

[Makarius]

On 13/09/16 01:46, Lawrence Paulson wrote:
> We have a problem with the ∄ operator, when existential quantifiers are nested:
> 
> lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))"
>   by (rule refl)
> 
> Note that ∄x y. P x y would be fine.

Looking briefly over this thread, my impression is that the simplest
solution is to disallow multiple variables for
∄ and ∃! as well.

We already have special quantifiers like ∃x:A that cannot be repeated
(for very basic technical reasons). This means users are used to
non-iterated quantifiers: it should cause less surprise than extra
syntax that is unclear.


	Makarius