[isabelle-dev] not-exists problem

Lawrence Paulson lp15 at cam.ac.uk
Wed Sep 14 11:54:01 CEST 2016

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.blanchette at inria.fr> 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.

More information about the isabelle-dev mailing list