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

[wren ng thornton]

On 8/15/12 12:32 PM, David Feuer wrote:
> On Aug 15, 2012 3:21 AM, "wren ng thornton"<wren at 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?

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