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