[isabelle-dev] not-exists problem
Peter Lammich
lammich at in.tum.de
Tue Sep 13 09:45:07 CEST 2016
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
More information about the isabelle-dev
mailing list