In classical logic A -> B is the equivalent to ~A v B<br>(with ~ = not and v = or)<br><br>So<br><br> (forall a. P(a)) -> Q<br>{implication = not-or}<br> ~(forall a. P(a)) v Q<br>{forall a. X is equivalent to there does not exist a such that X doesn't hold}<br>
~(~exists a. ~P(a)) v Q<br>{double negation elimination}<br> (exists a. ~P(a)) v Q<br>{a is not free in Q}<br> exists a. (~P(a) v Q)<br>{implication = not-or}<br> exists a. (P(a) -> Q)<br><br>These steps are all equivalencies, valid in both directions.<br>
<br><div class="gmail_quote">On Wed, Aug 15, 2012 at 9:32 AM, David Feuer <span dir="ltr"><<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im"><p>On Aug 15, 2012 3:21 AM, "wren ng thornton" <<a href="mailto:wren@freegeek.org" target="_blank">wren@freegeek.org</a>> wrote:<br>
> It's even easier than that.<br>
><br>
> (forall a. P(a)) -> Q <=> exists a. (P(a) -> Q)<br>
><br>
> 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.</p>
</div><p>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?</p>
<br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br>