THEOREM

******* 

The set of all things cannot exist.

 

~EXIST(s):[Set(s) & ALL(a):aes]

 

or equivalently...

 

ALL(s):[Set(s) => EXIST(a):~a e s]

 

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

    at http://www.dcproof.com )

 

 

PROOF

***** 

     Prove: ~EXIST(s):[Set(s) & ALL(a):a e s]

    

     Suppose to the contrary...

 

      1     Set(u) & ALL(a):a e u

            Premise

 

      2     Set(u)

            Split, 1

 

      3     ALL(a):a e u

            Split, 1

 

     Apply the Subset Axiom for u

 

      4     EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e u & ~a e a]]

            Subset, 2

 

     Define: r, the subset of all things that are not elements of themselves. (See Russell's Paradox, link here)

 

      5     Set(r) & ALL(a):[a e r <=> a e u & ~a e a]

            E Spec, 4

 

      6     Set(r)

            Split, 5

 

      7     ALL(a):[a e r <=> a e u & ~a e a]

            Split, 5

 

     Apply the definition of r to itself

 

      8     r e r <=> r e u & ~r e r

            U Spec, 7

 

      9     [r e r => r e u & ~r e r] & [r e u & ~r e r => r e r]

            Iff-And, 8

 

      10    r e r => r e u & ~r e r

            Split, 9

 

      11    r e u & ~r e r => r e r

            Split, 9

 

         

          Prove: ~r e r

         

          Suppose to the contrary...

 

            12    r e r

                  Premise

 

            13    r e u & ~r e r

                  Detach, 10, 12

 

            14    r e u

                  Split, 13

 

            15    ~r e r

                  Split, 13

 

          Obtain the contradiction...

 

            16    r e r & ~r e r

                  Join, 12, 15

 

     Apply the Conclusion Rule.

    

     As Required:

 

      17    ~r e r

            4 Conclusion, 12

 

     Apply the defintion of u to r

 

      18    r e u

            U Spec, 3

 

      19    r e u & ~r e r

            Join, 18, 17

 

      20    r e r

            Detach, 11, 19

 

     We obtain the contradicition...

 

      21    ~r e r & r e r

            Join, 17, 20

 

As Required:

 

22    ~EXIST(s):[Set(s) & ALL(a):a e s]

      4 Conclusion, 1

 

23    ~~ALL(s):~[Set(s) & ALL(a):a e s]

      Quant, 22

 

24    ALL(s):~[Set(s) & ALL(a):a e s]

      Rem DNeg, 23

 

25    ALL(s):~~[Set(s) => ~ALL(a):a e s]

      Imply-And, 24

 

26    ALL(s):[Set(s) => ~ALL(a):a e s]

      Rem DNeg, 25

 

27    ALL(s):[Set(s) => ~~EXIST(a):~a e s]

      Quant, 26

 

Or equivalently...

 

As Required:

 

28    ALL(s):[Set(s) => EXIST(a):~a e s]

      Rem DNeg, 27