The symmetry between the variables in ~(∃x y. P x y) is completely lost in ∄x.
∃y. P x y. It’s a terrible notation.
> On 13 Sep 2016, at 22:56, Jasmin Blanchette <jasmin.blanche...@inria.fr>
>> I’m not sure that this suggestion addresses my original problem: that the
>> use of the negated quantifier (by an output translation, i.e., not by
>> request) produced a confusing output. This output already contains only a
>> single variable bound by ∄.
> But to what extent do you find it confusing? Perhaps because our brains are
> damaged by too much logic and too little math, many of us on this list seemed
> to have no real issues parsing your example correctly.
isabelle-dev mailing list