INTRODUCTION
============
By Dan Christensen
Here we prove that
EXIST(b):[b e u & ALL(a):[a e u => P(a,b)]] (1)
does not necessarily follow from
ALL(a):[a e u => EXIST(b):[b e u & P(a,b)]] (2)
where u is the domain of quantification.
While, for some relations P, (1) and (2) can both be true, here we construct an example for which (1) is false and (2) is true:
We have the domain of quantification u = {0, 1}, and relation P such that P(a,b) iff a=b.
Outline
-------
First we list the required axioms/definitions.
Then we establish certain essential facts from these axioms/definitions:
0 e u
1 e u
P(0,0)
~P(0,1)
~P(1,0)
P(1,1)
Then we prove (2) is true: Every element of u has an equal, namely itself.
Finally, we prove (1) if false: No element of u is the equal of every element of u since ~0=1 and ~1=0.
AXIOMS/DEFINITIONS
==================
0 and 1 are distinct
1 ~0=1
Axiom
Define: u
2 ALL(a):[a e u <=> a=0 | a=1]
Axiom
Define: P
3 ALL(a):ALL(b):[a e u & b e u => [P(a,b) <=> a=b]]
Axiom
PROOF
=====
Establish essential facts
-------------------------
Prove: 0 e u
Apply definition of u
4 0 e u <=> 0=0 | 0=1
U Spec, 2
5 [0 e u => 0=0 | 0=1] & [0=0 | 0=1 => 0 e u]
Iff-And, 4
6 0 e u => 0=0 | 0=1
Split, 5
7 0=0 | 0=1 => 0 e u
Split, 5
8 0=0
Reflex
9 0=0 | 0=1
Arb Or, 8
As Required:
10 0 e u
Detach, 7, 9
Prove: 1 e u
Apply definition of u
11 1 e u <=> 1=0 | 1=1
U Spec, 2
12 [1 e u => 1=0 | 1=1] & [1=0 | 1=1 => 1 e u]
Iff-And, 11
13 1 e u => 1=0 | 1=1
Split, 12
14 1=0 | 1=1 => 1 e u
Split, 12
15 1=1
Reflex
16 1=0 | 1=1
Arb Or, 15
As Required:
17 1 e u
Detach, 14, 16
Prove: P(0,0)
Apply definition of P
18 ALL(b):[0 e u & b e u => [P(0,b) <=> 0=b]]
U Spec, 3
19 0 e u & 0 e u => [P(0,0) <=> 0=0]
U Spec, 18
20 0 e u & 0 e u
Join, 10, 10
21 P(0,0) <=> 0=0
Detach, 19, 20
22 [P(0,0) => 0=0] & [0=0 => P(0,0)]
Iff-And, 21
23 P(0,0) => 0=0
Split, 22
24 0=0 => P(0,0)
Split, 22
As Required:
25 P(0,0)
Detach, 24, 8
Prove: ~P(0,1)
Apply definition of P
26 0 e u & 1 e u => [P(0,1) <=> 0=1]
U Spec, 18
27 0 e u & 1 e u
Join, 10, 17
28 P(0,1) <=> 0=1
Detach, 26, 27
29 [P(0,1) => 0=1] & [0=1 => P(0,1)]
Iff-And, 28
30 P(0,1) => 0=1
Split, 29
31 0=1 => P(0,1)
Split, 29
32 ~0=1 => ~P(0,1)
Contra, 30
As Required:
33 ~P(0,1)
Detach, 32, 1
Prove: ~P(1,0)
Apply definition of P
34 ALL(b):[1 e u & b e u => [P(1,b) <=> 1=b]]
U Spec, 3
35 1 e u & 0 e u => [P(1,0) <=> 1=0]
U Spec, 34
36 1 e u & 0 e u
Join, 17, 10
37 P(1,0) <=> 1=0
Detach, 35, 36
38 [P(1,0) => 1=0] & [1=0 => P(1,0)]
Iff-And, 37
39 P(1,0) => 1=0
Split, 38
40 1=0 => P(1,0)
Split, 38
41 ~1=0 => ~P(1,0)
Contra, 39
42 ~0=1 => ~P(1,0)
Sym, 41
As Required:
43 ~P(1,0)
Detach, 42, 1
Prove: P(1,1)
44 1 e u & 1 e u => [P(1,1) <=> 1=1]
U Spec, 34
45 1 e u & 1 e u
Join, 17, 17
46 P(1,1) <=> 1=1
Detach, 44, 45
47 [P(1,1) => 1=1] & [1=1 => P(1,1)]
Iff-And, 46
48 P(1,1) => 1=1
Split, 47
49 1=1 => P(1,1)
Split, 47
As Required:
50 P(1,1)
Detach, 49, 15
Prove: ALL(a):[a e u => EXIST(b):[b e u & P(a,b)]]
Suppose...
51 x e u
Premise
Apply definition of u
52 x e u <=> x=0 | x=1
U Spec, 2
53 [x e u => x=0 | x=1] & [x=0 | x=1 => x e u]
Iff-And, 52
54 x e u => x=0 | x=1
Split, 53
55 x=0 | x=1 => x e u
Split, 53
Two cases:
56 x=0 | x=1
Detach, 54, 51
Case 1
Prove: x=0 => EXIST(b):[b e u & P(x,b)]
Suppose...
57 x=0
Premise
58 0 e u & P(0,0)
Join, 10, 25
59 0 e u & P(x,0)
Substitute, 57, 58
60 EXIST(b):[b e u & P(x,b)]
E Gen, 59
As Required:
61 x=0 => EXIST(b):[b e u & P(x,b)]
4 Conclusion, 57
Case 2
Prove: x=1 => EXIST(b):[b e u & P(x,b)]
Suppose...
62 x=1
Premise
63 1 e u & P(1,1)
Join, 17, 50
64 1 e u & P(x,1)
Substitute, 62, 63
65 EXIST(b):[b e u & P(x,b)]
E Gen, 64
As Required:
66 x=1 => EXIST(b):[b e u & P(x,b)]
4 Conclusion, 62
Join results
67 [x=0 => EXIST(b):[b e u & P(x,b)]]
& [x=1 => EXIST(b):[b e u & P(x,b)]]
Join, 61, 66
Apply Cases Rule
68 EXIST(b):[b e u & P(x,b)]
Cases, 56, 67
As Required:
69 ALL(a):[a e u => EXIST(b):[b e u & P(a,b)]]
4 Conclusion, 51
Prove: ALL(b):[b e u => EXIST(a):[a e u & ~P(a,b)]]
70 y e u
Premise
Apply definition of u
71 y e u <=> y=0 | y=1
U Spec, 2
72 [y e u => y=0 | y=1] & [y=0 | y=1 => y e u]
Iff-And, 71
73 y e u => y=0 | y=1
Split, 72
74 y=0 | y=1 => y e u
Split, 72
Two cases:
75 y=0 | y=1
Detach, 73, 70
Case 1
Prove: y=0 => EXIST(a):[a e u & ~P(a,y)]
Suppose...
76 y=0
Premise
77 1 e u & ~P(1,0)
Join, 17, 43
78 1 e u & ~P(1,y)
Substitute, 76, 77
79 EXIST(a):[a e u & ~P(a,y)]
E Gen, 78
As Required:
80 y=0 => EXIST(a):[a e u & ~P(a,y)]
4 Conclusion, 76
Case 2
Prove: y=1 => EXIST(a):[a e u & ~P(a,y)]
Suppose...
81 y=1
Premise
82 0 e u & ~P(0,1)
Join, 10, 33
83 0 e u & ~P(0,y)
Substitute, 81, 82
84 EXIST(a):[a e u & ~P(a,y)]
E Gen, 83
As Required:
85 y=1 => EXIST(a):[a e u & ~P(a,y)]
4 Conclusion, 81
Join results
86 [y=0 => EXIST(a):[a e u & ~P(a,y)]]
& [y=1 => EXIST(a):[a e u & ~P(a,y)]]
Join, 80, 85
Apply Cases Rule
87 EXIST(a):[a e u & ~P(a,y)]
Cases, 75, 86
As Required:
88 ALL(b):[b e u => EXIST(a):[a e u & ~P(a,b)]]
4 Conclusion, 70
Prove: ~EXIST(b):[b e u & ALL(a):[a e u => P(a,b)]]
89 ~EXIST(b):~[b e u => EXIST(a):[a e u & ~P(a,b)]]
Quant, 88
90 ~EXIST(b):~~[b e u & ~EXIST(a):[a e u & ~P(a,b)]]
Imply-And, 89
91 ~EXIST(b):[b e u & ~EXIST(a):[a e u & ~P(a,b)]]
Rem DNeg, 90
92 ~EXIST(b):[b e u & ~~ALL(a):~[a e u & ~P(a,b)]]
Quant, 91
93 ~EXIST(b):[b e u & ALL(a):~[a e u & ~P(a,b)]]
Rem DNeg, 92
94 ~EXIST(b):[b e u & ALL(a):~~[a e u => ~~P(a,b)]]
Imply-And, 93
95 ~EXIST(b):[b e u & ALL(a):[a e u => ~~P(a,b)]]
Rem DNeg, 94
As Required:
96 ~EXIST(b):[b e u & ALL(a):[a e u => P(a,b)]]
Rem DNeg, 95