This discussion clearly shows that ∃! with multiple bound variables is a recipe for confusion and should be avoided.

Tobias

On 14/09/2016 09:49, Peter Lammich wrote:
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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to