[isabelle-dev] not-exists problem

[Tobias Nipkow]

There is a method to this madness: if B is a binder, "B x y. t" is short for "B 
x. B y. t". However, I agree that for ∄ and ∃! this is confusing and one of the 
solutions proposed should be adopted.

Tobias

On 13/09/2016 09:45, Peter Lammich wrote:
> On Di, 2016-09-13 at 00:46 +0100, Lawrence Paulson wrote:
>> We have a problem with the ∄ operator, when existential quantifiers
>> are nested:
>>
>> lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))"
>>   by (rule refl)
>
> I do not see a particular problem with this, however, not-exists and
> also exists-one have funny semantics when used with multiple
> variables:
>
> lemma "(∄x y. P x y) ⟷ ¬(∃x. ¬(∃y. P x y))"
>     by (rule refl)
>
> lemma "(∃!x y. P x y) ⟷ (∃!x. (∃!y. P x y))"
>     by (rule refl)
>
> this leads to funny lemmas like:
>
> lemma not_what_you_might_think: "∄x y. x+y = (3::int)"
>   by presburger
>
> lemma also_strange: "∃!x y. x = abs (y::int)"
>   by (metis (no_types, hide_lams) abs_0_eq abs_minus_cancel
> equal_neg_zero)
>
>
> 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))
>
>
>
> We should either forbid multiple variables on those quantifiers, or try
> to figure out whether there is a widely-accepted consensus on their
> meaning.
>
> --
>   Peter
>
>
>>
>> Note that ∄x y. P x y would be fine.
>>
>> Larry
>>
>> ~/isabelle/Repos/src/HOL: hg id
>> dca6fabd8060 tip
>>
>> _______________________________________________
>> 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/20160913/50ecefcc/attachment.bin>