On 8/15/12 12:32 PM, David Feuer wrote:
On Aug 15, 2012 3:21 AM, "wren ng thornton"<w...@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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
