On 8/13/12 9:25 PM, Jay Sulzberger wrote:
I did suspect that, in some sense, "constraints" in combination
with "forall" could give the quantifier "exists".
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.
The duality mentioned previously is just for the case where you don't
have that handy "-> Q" there. How do we get the universal quantifier
into a negative position when there's no implication? Why, we add an
implication, of course. Even better, add two.
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
