[Haskell-cafe] forall & ST monad

[Kim-Ee Yeoh]

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.