[isabelle-dev] not-exists problem

[Michael.Norrish at data61.csiro.au]

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-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))
    
    +1
    
    Best,
    Tjark
    
    
    _______________________________________________
    isabelle-dev mailing list
    isabelle-dev at in.tum.de
    https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev