[isabelle-dev] not-exists problem

[Peter Lammich]

On Di, 2016-09-13 at 23:35 +0000, Michael.Norrish at 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-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/is
> abelle-dev
>     
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev