Here we resolve the existential fallacy:
All A are B
------------
Some A is B
In set theoretic notation...
Prove: ALL(u):ALL(pu):[Set(u)
& Set(pu)
& ALL(a):[a e pu <=> Set(a) & ALL(b):[b e a => b e u]]
=> ~ALL(a):ALL(b):[a e pu & b e pu => [ALL(c):[c e a => c e b] => EXIST(c):[c e a & c e b]]]]
We construct a counter-example with A and B being the null set.
(This proof was constructed with the aid of DC Proof 2.0. Download at http://www.dcproof.com )
Let pu be the power set of u
1 Set(u)
& Set(pu)
& ALL(a):[a e pu <=> Set(a) & ALL(b):[b e a => b e u]]
Premise
Splitting this premise...
2 Set(u)
Split, 1
3 Set(pu)
Split, 1
4 ALL(a):[a e pu <=> Set(a) & ALL(b):[b e a => b e u]]
Split, 1
Construct an empty subset of u
5 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e u & ~a=a]]
Subset, 2
6 Set(null) & ALL(a):[a e null <=> a e u & ~a=a]
E Spec, 5
Define: null, an empty subset of u
7 Set(null)
Split, 6
8 ALL(a):[a e null <=> a e u & ~a=a]
Split, 6
Prove: null e pu
Apply definition of pu
9 null e pu <=> Set(null) & ALL(b):[b e null => b e u]
U Spec, 4
10 [null e pu => Set(null) & ALL(b):[b e null => b e u]]
& [Set(null) & ALL(b):[b e null => b e u] => null e pu]
Iff-And, 9
11 null e pu => Set(null) & ALL(b):[b e null => b e u]
Split, 10
Sufficient: null e pu
12 Set(null) & ALL(b):[b e null => b e u] => null e pu
Split, 10
Prove: ALL(b):[b e null => b e u]
Suppose...
13 x e null
Premise
Apply definition of null
14 x e null <=> x e u & ~x=x
U Spec, 8
15 [x e null => x e u & ~x=x] & [x e u & ~x=x => x e null]
Iff-And, 14
16 x e null => x e u & ~x=x
Split, 15
17 x e u & ~x=x => x e null
Split, 15
18 x e u & ~x=x
Detach, 16, 13
19 x e u
Split, 18
As Required:
20 ALL(b):[b e null => b e u]
4 Conclusion, 13
Joining results...
21 Set(null) & ALL(b):[b e null => b e u]
Join, 7, 20
As Required:
22 null e pu
Detach, 12, 21
Prove: ALL(c):[c e null => c e null]
Suppose...
23 x e null
Premise
As Required:
24 ALL(c):[c e null => c e null]
4 Conclusion, 23
Prove: ~EXIST(a):a e null
Suppose to the contrary...
25 x e null
Premise
Apply definition of null
26 x e null <=> x e u & ~x=x
U Spec, 8
27 [x e null => x e u & ~x=x] & [x e u & ~x=x => x e null]
Iff-And, 26
28 x e null => x e u & ~x=x
Split, 27
29 x e u & ~x=x => x e null
Split, 27
30 x e u & ~x=x
Detach, 28, 25
31 x e u
Split, 30
32 ~x=x
Split, 30
Apply reflexivity of =
33 x=x
Reflex
34 x=x & ~x=x
Join, 33, 32
As Required:
null has no elements
35 ~EXIST(a):a e null
4 Conclusion, 25
Prove: ~EXIST(c):[c e null & c e null]
Suppose to the contrary...
36 x e null & x e null
Premise
37 x e null
Split, 36
38 x e null
Split, 36
Apply previous result
39 ~~ALL(a):~a e null
Quant, 35
40 ALL(a):~a e null
Rem DNeg, 39
41 ~x e null
U Spec, 40
42 x e null & ~x e null
Join, 38, 41
As Required:
43 ~EXIST(c):[c e null & c e null]
4 Conclusion, 36
Joining results...
44 null e pu & null e pu
Join, 22, 22
45 ALL(c):[c e null => c e null]
& ~EXIST(c):[c e null & c e null]
Join, 24, 43
46 null e pu & null e pu
& [ALL(c):[c e null => c e null]
& ~EXIST(c):[c e null & c e null]]
Join, 44, 45
47 EXIST(b):[null e pu & b e pu
& [ALL(c):[c e null => c e b]
& ~EXIST(c):[c e null & c e b]]]
E Gen, 46
48 EXIST(a):EXIST(b):[a e pu & b e pu
& [ALL(c):[c e a => c e b]
& ~EXIST(c):[c e a & c e b]]]
E Gen, 47
Change quantifiers, etc.
49 ~ALL(a):~EXIST(b):[a e pu & b e pu
& [ALL(c):[c e a => c e b]
& ~EXIST(c):[c e a & c e b]]]
Quant, 48
50 ~ALL(a):~~ALL(b):~[a e pu & b e pu
& [ALL(c):[c e a => c e b]
& ~EXIST(c):[c e a & c e b]]]
Quant, 49
51 ~ALL(a):ALL(b):~[a e pu & b e pu
& [ALL(c):[c e a => c e b]
& ~EXIST(c):[c e a & c e b]]]
Rem DNeg, 50
52 ~ALL(a):ALL(b):~~[a e pu & b e pu => ~[ALL(c):[c e a => c e b]
& ~EXIST(c):[c e a & c e b]]]
Imply-And, 51
53 ~ALL(a):ALL(b):[a e pu & b e pu => ~[ALL(c):[c e a => c e b]
& ~EXIST(c):[c e a & c e b]]]
Rem DNeg, 52
54 ~ALL(a):ALL(b):[a e pu & b e pu => ~~[ALL(c):[c e a => c e b] => ~~EXIST(c):[c e a & c e b]]]
Imply-And, 53
55 ~ALL(a):ALL(b):[a e pu & b e pu => [ALL(c):[c e a => c e b] => ~~EXIST(c):[c e a & c e b]]]
Rem DNeg, 54
56 ~ALL(a):ALL(b):[a e pu & b e pu => [ALL(c):[c e a => c e b] => EXIST(c):[c e a & c e b]]]
Rem DNeg, 55
As Required:
57 ALL(u):ALL(pu):[Set(u)
& Set(pu)
& ALL(a):[a e pu <=> Set(a) & ALL(b):[b e a => b e u]]
=> ~ALL(a):ALL(b):[a e pu & b e pu => [ALL(c):[c e a => c e b] => EXIST(c):[c e a & c e b]]]]
4 Conclusion, 1