Jonathan Cast 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.

jcc

```