Theorem
-------
The statement
EXIST(b):[b e u & ALL(a):[a e u => P(a,b)]] (1)
does NOT follow from the statement
ALL(a):[a e u => EXIST(b):[b e u & P(a,b)]] (2)
As proof, we present a simple counter-example: We let the domain of quantification u = {x, y} for distinct x and y, and let the predicate P be the "is equal to" relation defined on u.
Note: The fact that x and y are distinct follows from the axioms P(x,x) and ~P(x,y). Assuming x=y would lead to a contradiction.
We will prove that, in this case, (1) is false and (2) is true.
By Dan Christensen
Axioms
------
Define: u, the domain of quantification
Note: '|' is the OR-operator in DC Proof
1 ALL(a):[a e u <=> a=x | a=y]
Axiom
We will require: x e u
Apply definition of u
2 x e u <=> x=x | x=y
U Spec, 1
3 [x e u => x=x | x=y] & [x=x | x=y => x e u]
Iff-And, 2
4 x e u => x=x | x=y
Split, 3
5 x=x | x=y => x e u
Split, 3
6 x=x
Reflex
7 x=x | x=y
Arb Or, 6
8 x e u
Detach, 5, 7
We will also require y e u
Apply definition of u
9 y e u <=> y=x | y=y
U Spec, 1
10 [y e u => y=x | y=y] & [y=x | y=y => y e u]
Iff-And, 9
11 y e u => y=x | y=y
Split, 10
12 y=x | y=y => y e u
Split, 10
13 y=y
Reflex
14 y=x | y=y
Arb Or, 13
15 y e u
Detach, 12, 14
Define: P (the relation "is equal to" on u)
16 P(x,x)
Axiom
17 P(y,y)
Axiom
18 ~P(x,y)
Axiom
19 ~P(y,x)
Axiom
Proof
-----
Prove: ALL(a):[a e u => EXIST(b):[b e u & P(a,b)]]
Suppose...
20 v e u
Premise
Apply definition of u
21 v e u <=> v=x | v=y
U Spec, 1
22 [v e u => v=x | v=y] & [v=x | v=y => v e u]
Iff-And, 21
23 v e u => v=x | v=y
Split, 22
24 v=x | v=y => v e u
Split, 22
2 cases:
25 v=x | v=y
Detach, 23, 20
Case 1
Prove: v=x => EXIST(b):[b e u & P(v,b)]
Suppose...
26 v=x
Premise
27 x e u & P(x,x)
Join, 8, 16
28 x e u & P(v,x)
Substitute, 26, 27
29 EXIST(b):[b e u & P(v,b)]
E Gen, 28
As Required:
30 v=x => EXIST(b):[b e u & P(v,b)]
4 Conclusion, 26
Case 2
Prove: v=y => EXIST(b):[b e u & P(v,b)]
Suppose...
31 v=y
Premise
32 y e u & P(y,y)
Join, 15, 17
33 y e u & P(v,y)
Substitute, 31, 32
34 EXIST(b):[b e u & P(v,b)]
E Gen, 33
As Required:
35 v=y => EXIST(b):[b e u & P(v,b)]
4 Conclusion, 31
Join results for Cases Rule
36 [v=x => EXIST(b):[b e u & P(v,b)]]
& [v=y => EXIST(b):[b e u & P(v,b)]]
Join, 30, 35
Apply Cases Rule
37 EXIST(b):[b e u & P(v,b)]
Cases, 25, 36
As Required:
38 ALL(a):[a e u => EXIST(b):[b e u & P(a,b)]]
4 Conclusion, 20
Prove: ALL(b):[b e u => EXIST(a):[a e u & ~P(a,b)]]
Suppose...
39 w e u
Premise
Apply definition of u
40 w e u <=> w=x | w=y
U Spec, 1
41 [w e u => w=x | w=y] & [w=x | w=y => w e u]
Iff-And, 40
42 w e u => w=x | w=y
Split, 41
43 w=x | w=y => w e u
Split, 41
2 cases:
44 w=x | w=y
Detach, 42, 39
Case 1
Prove: w=x => EXIST(a):[a e u & ~P(a,w)]
Suppose...
45 w=x
Premise
46 y e u & ~P(y,x)
Join, 15, 19
47 y e u & ~P(y,w)
Substitute, 45, 46
48 EXIST(a):[a e u & ~P(a,w)]
E Gen, 47
As Required:
49 w=x => EXIST(a):[a e u & ~P(a,w)]
4 Conclusion, 45
Case 2
Prove: w=y => EXIST(a):[a e u & ~P(a,w)]
Suppose...
50 w=y
Premise
51 x e u & ~P(x,y)
Join, 8, 18
52 x e u & ~P(x,w)
Substitute, 50, 51
53 EXIST(a):[a e u & ~P(a,w)]
E Gen, 52
As Required:
54 w=y => EXIST(a):[a e u & ~P(a,w)]
4 Conclusion, 50
Join results for Cases Rule
55 [w=x => EXIST(a):[a e u & ~P(a,w)]]
& [w=y => EXIST(a):[a e u & ~P(a,w)]]
Join, 49, 54
Apply Cases Rule
56 EXIST(a):[a e u & ~P(a,w)]
Cases, 44, 55
As Required:
57 ALL(b):[b e u => EXIST(a):[a e u & ~P(a,b)]]
4 Conclusion, 39
Prove: ~EXIST(b):[b e u & ALL(a):[a e u => P(a,b)]]
58 ~EXIST(b):~[b e u => EXIST(a):[a e u & ~P(a,b)]]
Quant, 57
59 ~EXIST(b):~~[b e u & ~EXIST(a):[a e u & ~P(a,b)]]
Imply-And, 58
60 ~EXIST(b):[b e u & ~EXIST(a):[a e u & ~P(a,b)]]
Rem DNeg, 59
61 ~EXIST(b):[b e u & ~~ALL(a):~[a e u & ~P(a,b)]]
Quant, 60
62 ~EXIST(b):[b e u & ALL(a):~[a e u & ~P(a,b)]]
Rem DNeg, 61
63 ~EXIST(b):[b e u & ALL(a):~~[a e u => ~~P(a,b)]]
Imply-And, 62
64 ~EXIST(b):[b e u & ALL(a):[a e u => ~~P(a,b)]]
Rem DNeg, 63
As Required:
65 ~EXIST(b):[b e u & ALL(a):[a e u => P(a,b)]]
Rem DNeg, 64