<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<p><font size="+1">The desired multi-variable semantics of ∄ seem
obvious enough to me and I think that this should be allowed.</font></p>
<p><font size="+1">For ∃!, the implicit complexity introduced by the
pairing seems too much to me, so I think this should be
forbidden.<br>
</font></p>
<br>
<div class="moz-cite-prefix">On 13/09/16 10:41, Johannes Hölzl
wrote:<br>
</div>
<blockquote cite="mid:1473756118.5222.32.camel@in.tum.de"
type="cite">
<pre wrap="">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:
</pre>
<blockquote type="cite">
<pre wrap="">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:
</pre>
<blockquote type="cite">
<pre wrap="">
On Di, 2016-09-13 at 00:46 +0100, Lawrence Paulson wrote:
</pre>
<blockquote type="cite">
<pre wrap="">
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)
</pre>
</blockquote>
<pre wrap="">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
</pre>
<blockquote type="cite">
<pre wrap="">
Note that ∄x y. P x y would be fine.
Larry
~/isabelle/Repos/src/HOL: hg id
dca6fabd8060 tip
_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is</a>
abel
le-dev
</pre>
</blockquote>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab</a>
elle-dev
</pre>
</blockquote>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel</a>
le-dev
</pre>
</blockquote>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>