On Di, 2016-09-13 at 23:35 +0000, michael.norr...@data61.csiro.au wrote: > Note that ∃!x. ∃!y. P x y is not equivalent to ∃!xy. P (fst xy) (snd > xy). > > If you were going to support ∃!x y at all (and I can certainly see > the argument for forbidding it outright), I'd expect it to map to the > first formula above, and not the second.
So there seems to be no consensus on the meaning of "∃!x y". Btw: I would strongly argue that a proposition like "∃!x y. x = abs (y::int)" is wrong, however it holds with the "∃!x. ∃!y"-semantics. -- Peter > > Michael > > On 13/09/2016, 18:41, "isabelle-dev on behalf of Tjark Weber" <isabel > le-dev-boun...@mailbroy.informatik.tu-muenchen.de on behalf of tjark. > we...@it.uu.se> wrote: > > On Tue, 2016-09-13 at 09:45 +0200, Peter Lammich wrote: > > I would have expected: > > (∄x y. P x y) ⟷ ¬(∃x y. P x y) > > and > > (∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x)) > > +1 > > Best, > Tjark > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is > abelle-dev > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel > le-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev