THEOREM
-------
For every set s there exists an empty subset of s
ALL(s):[Set(s)
=> EXIST(null):[Set(null) & ALL(a):[a e null => a e s]
& ~EXIST(a):a e null]]
This formal proof was prepared with the use of the author's DC Proof 2.0 software
available at http://www.dcproof.com
PROOF
-----
Let s be a set
1 Set(s)
Premise
Apply the Subset Axiom (similar to Specification in ZF)
Select a subset of s using selection criteria that cannot be met (that the elements
are not equal to themselves)
2 EXIST(a):[Set(a) & ALL(b):[b e a <=> b e s & ~b=b]]
Subset, 1
Define: the null set
3 Set(null) & ALL(b):[b e null <=> b e s & ~b=b]
E Spec, 2
Splitting this definition into it component parts...
4 Set(null)
Split, 3
5 ALL(b):[b e null <=> b e s & ~b=b]
Split, 3
Show that null is empty
Prove: ~EXIST(a):a e null
Suppose to the contrary...
6 x e null
Premise
Apply the definition of null
7 x e null <=> x e s & ~x=x
U Spec, 5
8 [x e null => x e s & ~x=x] & [x e s & ~x=x => x e null]
Iff-And, 7
9 x e null => x e s & ~x=x
Split, 8
10 x e s & ~x=x => x e null
Split, 8
11 x e s & ~x=x
Detach, 9, 6
12 x e s
Split, 11
13 ~x=x
Split, 11
14 x=x
Reflex
Obtain the contradiction...
15 x=x & ~x=x
Join, 14, 13
null is empty
As Required:
16 ~EXIST(a):a e null
4 Conclusion, 6
Joining previous results...
17 Set(null) & ~EXIST(a):a e null
Join, 4, 16
Prove: null is a subset of s
Suppose...
18 y e null
Premise
Apply the definition of null
19 y e null <=> y e s & ~y=y
U Spec, 5
20 [y e null => y e s & ~y=y] & [y e s & ~y=y => y e null]
Iff-And, 19
21 y e null => y e s & ~y=y
Split, 20
22 y e s & ~y=y => y e null
Split, 20
23 y e s & ~y=y
Detach, 21, 18
24 y e s
Split, 23
null is a subset of s
As Required:
25 ALL(a):[a e null => a e s]
4 Conclusion, 18
26 Set(null) & ALL(a):[a e null => a e s]
Join, 4, 25
27 Set(null) & ALL(a):[a e null => a e s]
& ~EXIST(a):a e null
Join, 26, 16
As Required:
28 ALL(s):[Set(s)
=> EXIST(null):[Set(null) & ALL(a):[a e null => a e s]
& ~EXIST(a):a e null]]
4 Conclusion, 1