THEOREM

*******

EXIST(x):[S(x) => Q]  is not true in general, e.g. when ALL(a):S(a) is true and Q is false

(This proof was written with the aid of the author's DC Proof 2.0 software available

at http://www.dcproof.com)

PROOF

*****

Suppose...

1     ALL(a):S(a)

      Axiom

Suppose Q is false

2     ~Q

      Axiom

     Prove: ~EXIST(x):[S(x) => Q]

     Suppose to the contrary...

      3     EXIST(x):[S(x) => Q]

            Premise

      4     S(x) => Q

            E Spec, 3

      5     S(x)

            U Spec, 1

      6     Q

            Detach, 4, 5

     Obtain the contradiction...

      7     Q & ~Q

            Join, 6, 2

As Required:

8     ~EXIST(x):[S(x) => Q]

      4 Conclusion, 3