[isabelle-dev] not-exists problem

Michael.Norrish at data61.csiro.au Michael.Norrish at data61.csiro.au
Wed Sep 14 01:35:54 CEST 2016

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.


On 13/09/2016, 18:41, "isabelle-dev on behalf of Tjark Weber" <isabelle-dev-bounces at mailbroy.informatik.tu-muenchen.de on behalf of tjark.weber at 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))
    isabelle-dev mailing list
    isabelle-dev at in.tum.de

More information about the isabelle-dev mailing list