Re: [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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
le-dev

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev