[isabelle-dev] not-exists problem
Jasmin Blanchette
jasmin.blanchette at inria.fr
Tue Sep 13 10:12:50 CEST 2016
> On 13.09.2016, at 09:45, Peter Lammich <lammich at in.tum.de> 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,
Like you I find ∄x. ∃y. P x y clear (albeit weird), but ∄x y. P x y is probably a better way to display the same thing.
> lemma "(∄x y. P x y) ⟷ ¬(∃x. ¬(∃y. P x y))"
> by (rule refl)
That looks like a serious flaw.
> lemma "(∃!x y. P x y) ⟷ (∃!x. (∃!y. P x y))"
> by (rule refl)
Ditto.
> We should either forbid multiple variables on those quantifiers, or try
> to figure out whether there is a widely-accepted consensus on their
> meaning.
The best would be to forbid multiple variables for ∃!. For ∄, the situation is more complicated. We can forbid them, or we can interpret a single multi-variable ∄ as ∄∃...∃ (and in the other direction for printing).
Jasmin
More information about the isabelle-dev
mailing list