[isabelle-dev] not-exists problem

[Johannes Hölzl]

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