[Haskell-cafe] forall & ST monad

[Jonathan Cast]

On Wed, 2009-02-25 at 10:18 -0800, Kim-Ee Yeoh wrote:
> 
> 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

[For the record: this is the first point at which you confine yourself
to classical logic.]

> = not $ (forall a. T(a)) and (not S), by de Morgan's
> = not $ forall a. T(a) and (not S), product rule???

This step depends on the domain of quantification for the variable a
being non-empty; if the domain is empty, then the RHS is vacuously true,
while the LHS is equal to (not S).

> = 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.

jcc