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 <> 
> wrote:
>> 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

Reply via email to