<br><br><div class="gmail_quote">On Thu, Aug 16, 2012 at 8:07 PM, wren ng thornton <span dir="ltr"><<a href="mailto:wren@freegeek.org" target="_blank">wren@freegeek.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im">On 8/15/12 2:55 PM, Albert Y. C. Lai wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On 12-08-15 03:20 AM, wren ng thornton wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
(forall a. P(a)) -> Q <=> exists a. (P(a) -> Q)<br>
</blockquote>
<br>
For example:<br>
<br>
A. (forall p. p drinks) -> (everyone drinks)<br>
B. exists p. ((p drinks) -> (everyone drinks))<br>
<br>
In a recent poll, 100% of respondents think A true, 90% of them think B<br>
paradoxical, and 40% of them have not heard of the Smullyan drinking<br>
paradox.<br>
</blockquote>
<br></div>
:)<br>
<br>
Though bear in mind we're discussing second-order quantification here, not first-order.</blockquote><div><br></div><div>Can you expand on what you mean here? I don't see two kinds of quantification in the type language (at least, reflexively, in the context of what we're discussing). In particular, I don't see how to quantify over predicates for (or sets of, via the extensions of the predicates) types.</div>
<div><br></div><div>Is Haskell's 'forall' doing double duty?</div></div>