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 = n (the set of natural numbers), and relation P such that P(a,b) iff b>a.
Outline
-------
First we list the required axioms/definitions.
Then we establish certain essential facts from these axioms/definitions:
Then we prove (2) is true: Every element of n has number greater element of n.
Finally, we prove (1) if false: No element of n greater than all other elements of n.
AXIOMS/DEFINITIONS
==================
Let the domain of quantification u be the set of natural numbers n
1 u=n
Axiom
Define: P
P(a,b) means b>a
2 ALL(a):ALL(b):[a e n & b e n => [P(a,b) <=> b>a]]
Axiom
Essential Properties of n and >
-------------------------------
Property 1:
3 ALL(a):[a e n => EXIST(b):[b e n & b>a]]
Axiom
Property 2:
4 ALL(a):ALL(b):[a e n & b e n => [a>b => ~b>a]]
Axiom
PROOF
=====
Prove: ALL(a):[aen => EXIST(b): [ben & P(a,b]]
Suppose...
5 x e n
Premise
Apply Property 1
6 x e n => EXIST(b):[b e n & b>x]
U Spec, 3
7 EXIST(b):[b e n & b>x]
Detach, 6, 5
Define: y
8 y e n & y>x
E Spec, 7
9 y e n
Split, 8
10 y>x
Split, 8
Apply definition of P
11 ALL(b):[x e n & b e n => [P(x,b) <=> b>x]]
U Spec, 2
12 x e n & y e n => [P(x,y) <=> y>x]
U Spec, 11
13 x e n & y e n
Join, 5, 9
14 P(x,y) <=> y>x
Detach, 12, 13
15 [P(x,y) => y>x] & [y>x => P(x,y)]
Iff-And, 14
16 P(x,y) => y>x
Split, 15
17 y>x => P(x,y)
Split, 15
18 P(x,y)
Detach, 17, 10
19 y e n & P(x,y)
Join, 9, 18
As Required:
20 ALL(a):[a e n => EXIST(b):[b e n & P(a,b)]]
4 Conclusion, 5
21 ALL(a):[a e u => EXIST(b):[b e u & P(a,b)]]
Substitute, 1, 20
Prove: ALL(b):[b e n => EXIST(a):[a e n & ~P(a,b)]]
Suppose...
22 y e n
Premise
Apply Property 2
23 y e n => EXIST(b):[b e n & b>y]
U Spec, 3
24 EXIST(b):[b e n & b>y]
Detach, 23, 22
Define: x
25 x e n & x>y
E Spec, 24
26 x e n
Split, 25
27 x>y
Split, 25
Apply definition of P
28 ALL(b):[x e n & b e n => [P(x,b) <=> b>x]]
U Spec, 2
29 x e n & y e n => [P(x,y) <=> y>x]
U Spec, 28
30 x e n & y e n
Join, 26, 22
31 P(x,y) <=> y>x
Detach, 29, 30
32 [P(x,y) => y>x] & [y>x => P(x,y)]
Iff-And, 31
33 P(x,y) => y>x
Split, 32
34 y>x => P(x,y)
Split, 32
Sufficient: For ~P(x,y)
35 ~y>x => ~P(x,y)
Contra, 33
Prove: ~y>x
Apply Property 2
36 ALL(b):[x e n & b e n => [x>b => ~b>x]]
U Spec, 4
37 x e n & y e n => [x>y => ~y>x]
U Spec, 36
38 x e n & y e n
Join, 26, 22
39 x>y => ~y>x
Detach, 37, 38
As Required:
40 ~y>x
Detach, 39, 27
41 ~P(x,y)
Detach, 35, 40
42 x e n & ~P(x,y)
Join, 26, 41
As Required:
43 ALL(b):[b e n => EXIST(a):[a e n & ~P(a,b)]]
4 Conclusion, 22
Prove: ~EXIST(b):[b e u & ALL(a):[a e u => P(a,b)]
44 ALL(b):[b e u => EXIST(a):[a e u & ~P(a,b)]]
Substitute, 1, 43
45 ~EXIST(b):~[b e u => EXIST(a):[a e u & ~P(a,b)]]
Quant, 44
46 ~EXIST(b):~~[b e u & ~EXIST(a):[a e u & ~P(a,b)]]
Imply-And, 45
47 ~EXIST(b):[b e u & ~EXIST(a):[a e u & ~P(a,b)]]
Rem DNeg, 46
48 ~EXIST(b):[b e u & ~~ALL(a):~[a e u & ~P(a,b)]]
Quant, 47
49 ~EXIST(b):[b e u & ALL(a):~[a e u & ~P(a,b)]]
Rem DNeg, 48
50 ~EXIST(b):[b e u & ALL(a):~~[a e u => ~~P(a,b)]]
Imply-And, 49
51 ~EXIST(b):[b e u & ALL(a):[a e u => ~~P(a,b)]]
Rem DNeg, 50
As Required:
52 ~EXIST(b):[b e u & ALL(a):[a e u => P(a,b)]]
Rem DNeg, 51