[Haskell-cafe] Data structure containing elements which are instances of the same type class

[David Feuer]

I understand this now, though I still don't understand the context. Thanks!
I managed to mix up implication with causation, to my great embarrassment.
On Aug 15, 2012 3:39 PM, "Ryan Ingram" <ryani.spam at gmail.com> wrote:

> In classical logic  A -> B is the equivalent to ~A v B
> (with ~ = not and v = or)
>
> So
>
>     (forall a. P(a)) -> Q
> {implication = not-or}
>     ~(forall a. P(a)) v Q
> {forall a. X is equivalent to there does not exist a such that X doesn't
> hold}
>     ~(~exists a. ~P(a)) v Q
> {double negation elimination}
>     (exists a. ~P(a)) v Q
> {a is not free in Q}
>     exists a. (~P(a) v Q)
> {implication = not-or}
>     exists a. (P(a) -> Q)
>
> These steps are all equivalencies, valid in both directions.
>
> On Wed, Aug 15, 2012 at 9:32 AM, David Feuer <david.feuer at gmail.com>wrote:
>
>> On Aug 15, 2012 3:21 AM, "wren ng thornton" <wren at freegeek.org> wrote:
>> > It's even easier than that.
>> >
>> >     (forall a. P(a)) -> Q  <=>  exists a. (P(a) -> Q)
>> >
>> > Where P and Q are metatheoretic/schematic variables. This is just the
>> usual thing about antecedents being in a "negative" position, and thus
>> flipping as you move into/out of that position.
>>
>> Most of this conversation is going over my head. I can certainly see how
>> exists a. (P(a)->Q) implies that (forall a. P(a))->Q. The opposite
>> certainly doesn't hold in classical logic. What sort of logic are you folks
>> working in?
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120815/f5a6b428/attachment.htm>