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@gmail.com> wrote:

On Aug 15, 2012 3:21 AM, "wren ng thornton" <wren@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