[Haskell-cafe] forall & ST monad
jonathanccast at fastmail.fm
Wed Feb 25 13:20:32 EST 2009
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.
More information about the Haskell-Cafe