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. _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
