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.


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
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
also exists-one have funny semantics when used with multiple

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

I would have expected:
(∄x y. P x y) ⟷ ¬(∃x y. P x y)
(∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))

We should either forbid multiple variables on those quantifiers, or
to figure out whether there is a widely-accepted consensus on their


Note that ∄x y. P x y would be fine.


~/isabelle/Repos/src/HOL: hg id
dca6fabd8060 tip

isabelle-dev mailing list
isabelle-dev mailing list

isabelle-dev mailing list
isabelle-dev mailing list

isabelle-dev mailing list

Reply via email to