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.
Michael
On 13/09/2016, 18:41, "isabelle-dev on behalf of Tjark Weber"
<isabelle-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/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
