THEOREM
-------
There is only one empty set. If null and null' are empty sets, then null = 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
-----
Suppose null and null' are empty sets
1 Set(null) & ~EXIST(a):a e null
& Set(null') & ~EXIST(a):a e null'
Premise
Splitting this premise into its component parts...
2 Set(null)
Split, 1
3 ~EXIST(a):a e null
Split, 1
4 Set(null')
Split, 1
5 ~EXIST(a):a e null'
Split, 1
Apply the Set Equality Axiom (similar to Extensionality in ZF)
6 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]
Set Equality
7 ALL(b):[Set(null) & Set(b) => [null=b <=> ALL(c):[c e null <=> c e b]]]
U Spec, 6
8 Set(null) & Set(null') => [null=null' <=> ALL(c):[c e null <=> c e null']]
U Spec, 7
9 Set(null) & Set(null')
Join, 2, 4
Necessary and sufficient condition for null=null'
10 null=null' <=> ALL(c):[c e null <=> c e null']
Detach, 8, 9
11 [null=null' => ALL(c):[c e null <=> c e null']]
& [ALL(c):[c e null <=> c e null'] => null=null']
Iff-And, 10
12 null=null' => ALL(c):[c e null <=> c e null']
Split, 11
Sufficient condition for null=null'
13 ALL(c):[c e null <=> c e null'] => null=null'
Split, 11
'=>'
Prove: ALL(c):[c e null => c e null']
Suppose...
14 x e null
Premise
Apply definition of null
Switch quantifier
15 ~~ALL(a):~a e null
Quant, 3
Remove '~~'
16 ALL(a):~a e null
Rem DNeg, 15
17 ~x e null
U Spec, 16
Anything follows from a falsehood
Apply Arbitrary Consequent Rule
18 ~~x e null => x e null'
Arb Cons, 17
19 x e null => x e null'
Rem DNeg, 18
20 x e null'
Detach, 19, 14
As Required:
21 ALL(c):[c e null => c e null']
4 Conclusion, 14
'<='
Similarly prove: ALL(c):[c e null' => c e null]
Suppose...
22 x e null'
Premise
23 ~~ALL(a):~a e null'
Quant, 5
24 ALL(a):~a e null'
Rem DNeg, 23
25 ~x e null'
U Spec, 24
26 ~~x e null' => x e null
Arb Cons, 25
27 x e null' => x e null
Rem DNeg, 26
28 x e null
Detach, 27, 22
As Required:
29 ALL(c):[c e null' => c e null]
4 Conclusion, 22
30 ALL(c):[[c e null => c e null'] & [c e null' => c e null]]
Join, 21, 29
31 ALL(c):[c e null <=> c e null']
Iff-And, 30
As Required:
32 null=null'
Detach, 13, 31