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
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