[Haskell-cafe] Data structure containing elements which are instances of the same type class
wren ng thornton
wren at freegeek.org
Fri Aug 17 05:05:29 CEST 2012
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.
More information about the Haskell-Cafe