Heinrich Apfelmus wrote:
Now,
(forall a. T[a]) -> S
is clearly true while
exists a. (T[a] -> S)
should be nonsense: having one example of a marble that is either red or blue does in no way imply that all of them are, at least constructively. (It is true classically, but I forgot the name of the corresponding theorem.)
For the record, allow me to redress my earlier erroneous assertion by furnishing the proof for the classical case: (forall a. T(a)) -> S = not (forall a. T(a)) or S, by defn of implication = not $ (forall a. T(a)) and (not S), by de Morgan's = not $ forall a. T(a) and (not S), product rule??? = exists a. not (T(a)) or S, de Morgan's again = exists a. T(a) -> S, by defn of implication The only wrinkle is obviously in the logical "and" of (not S) distributing under the universal quantifier. -- View this message in context: http://www.nabble.com/forall---ST-monad-tp22024677p22208626.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.