[isabelle-dev] not-exists problem

[Tobias Nipkow]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160914/dafc88ba/attachment.bin>