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