Re: [Haskell-cafe] Data structure containing elements which are instances of the same type class

On 8/15/12 12:32 PM, David Feuer wrote:

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

Ryan gave a nice classical proof. Though note that, in a constructive setting you're right to be dubious. The validity of the questioned article is related to the "generalized Markov's principle" which Russian constructivists accept but which is not derivable from Heyting's axiomatization of intuitionistic logic: GMP : ~(forall x. P(x)) -> (exists x. ~P(x)) There's been a fair amount of work on showing that GMP is constructively valid; though the fact that it does not derive from Heyting's axiomatization makes some squeamish. For these reasons it may be preferable to stick with the double-negation form upthread for converting between quantifiers. I just mentioned the above as a simplification of the double-negation form, which may be more familiar to those indoctrinated in classical logic. -- Live well, ~wren