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. Larry
> On 13 Sep 2016, at 22:56, Jasmin Blanchette <jasmin.blanche...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
