THEOREM

*******

 

  ALL(a):[EXIST(b):P(b) => P(a) <=> ALL(b):[P(b) => P(a)]]

 

 

This proof was written and verified with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com

 

    

     PROOF

     *****

    

     '=>'

    

     Prove: ALL(a):[EXIST(b):P(b) => P(a) => ALL(b):[P(b) => P(a)]]

    

     Suppose...

 

      1     EXIST(b):P(b) => P(y)

            Premise

 

         

          Prove: ALL(b):[P(b) => P(y)]

         

          Suppose...

 

            2     P(x)

                  Premise

 

            3     EXIST(b):P(b)

                  E Gen, 2

 

            4     P(y)

                  Detach, 1, 3

 

     As Required:

 

      5     ALL(b):[P(b) => P(y)]

            4 Conclusion, 2

 

As Required:

 

6     ALL(a):[EXIST(b):P(b) => P(a) => ALL(b):[P(b) => P(a)]]

      4 Conclusion, 1

 

    

     '<='

    

     Prove: ALL(a):[ALL(b):[P(b) => P(a)] => [EXIST(b):P(b) => P(a)]]

    

     Suppose...

 

      7     ALL(b):[P(b) => P(y)]

            Premise

 

         

          Prove: EXIST(b):P(b) => P(y)

         

          Suppose...

 

            8     EXIST(b):P(b)

                  Premise

 

            9     P(x)

                  E Spec, 8

 

            10    P(x) => P(y)

                  U Spec, 7

 

            11    P(y)

                  Detach, 10, 9

 

     As Required:

 

      12    EXIST(b):P(b) => P(y)

            4 Conclusion, 8

 

As Required:

 

13    ALL(a):[ALL(b):[P(b) => P(a)] => [EXIST(b):P(b) => P(a)]]

      4 Conclusion, 7

 

Joining results...

 

14    ALL(a):[[EXIST(b):P(b) => P(a) => ALL(b):[P(b) => P(a)]]

     & [ALL(b):[P(b) => P(a)] => [EXIST(b):P(b) => P(a)]]]

      Join, 6, 13

 

 

As Required:

 

15    ALL(a):[EXIST(b):P(b) => P(a)

     <=> ALL(b):[P(b) => P(a)]]

      Iff-And, 14