[isabelle-dev] not-exists problem

[Manuel Eberl]

The desired multi-variable semantics of ∄ seem obvious enough to me and 
I think that this should be allowed.

For ∃!, the implicit complexity introduced by the pairing seems too much 
to me, so I think this should be forbidden.


On 13/09/16 10:41, Johannes Hölzl wrote:
> There is even a third one: ∄!
>
> I would vote to forbid the multiple variable case. At least for the
> next release. Is it possible to restrict this by a mixfix syntax or
> does it require to write a ML parse translations.
>
>   - Johannes
>
> Am Dienstag, den 13.09.2016, 10:30 +0200 schrieb 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/is
>>>> abel
>>>> le-dev
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab
>>> elle-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 --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160913/feff9279/attachment-0002.html>