[Haskell-cafe] Data structure containing elements which are instances of the same type class
Ryan Ingram
ryani.spam at gmail.com
Wed Aug 15 21:39:10 CEST 2012
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/0790bf7f/attachment.htm>
More information about the Haskell-Cafe
mailing list