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