[Haskell-cafe] forall & ST monad
a.biurvOir4 at asuhan.com
Wed Feb 25 13:18:45 EST 2009
Heinrich Apfelmus wrote:
> (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
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.
More information about the Haskell-Cafe