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.s...@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.fe...@gmail.com>wrote: > >> On Aug 15, 2012 3:21 AM, "wren ng thornton" <w...@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@haskell.org >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> >> >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe