THEOREM
*******
The intersection of {{0, 1, ...},
{1, 2, ...}, {2, 3, ...}, ...} = {}
where {0, 1, ...}, {1, 3, ...},
{2, 3, ...}, etc. are the "end segments" in N.
Here, we prove:
~EXIST(a):ALL(b):[b
e ends => a e b]
where (informally)
ends = {{0, 1, ...}, {1, 2, ...}, {2, 3,
...}, ...}
The following proof makes use
of the set theoretic axioms for subsets (lines 12, 18) and power sets (line 6).
This formal, machine-verified
proof was write with the aid of the author's DC Proof 2.0 software available at
http://www.dcproof.com
AXIOMS
******
1 Set(n)
Axiom
2 0 e n
Axiom
3 ALL(a):[a e n => ~a<a]
Axiom
4 ALL(a):ALL(b):[a e n & b e n => [a<=b <=> a<b | a=b]]
Axiom
5 ALL(a):[a e n => 0<=a]
Axiom
PROOF
*****
Construct the power set of n
Apply the Power Set Axiom
6 ALL(a):[Set(a) => EXIST(b):[Set(b)
&
ALL(c):[c e b <=>
Set(c) & ALL(d):[d e c => d e a]]]]
Power Set
7 Set(n) => EXIST(b):[Set(b)
&
ALL(c):[c e b <=>
Set(c) & ALL(d):[d e c => d e n]]]
U Spec, 6
8 EXIST(b):[Set(b)
&
ALL(c):[c e b <=>
Set(c) & ALL(d):[d e c => d e n]]]
Detach, 7, 1
9 Set(pn)
&
ALL(c):[c e pn <=> Set(c) & ALL(d):[d e c => d e n]]
E Spec, 8
Define: pn
10 Set(pn)
Split, 9
11 ALL(c):[c e pn <=> Set(c) & ALL(d):[d e c => d e n]]
Split, 9
Construct the set of end
segments
12 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e pn &
EXIST(b):[b e n & ALL(c):[c e a =>
b<=c]]]]
Subset, 10
13 Set(ends) & ALL(a):[a e ends <=> a e pn &
EXIST(b):[b e n & ALL(c):[c e a =>
b<=c]]]
E Spec, 12
Define: ends
Informally, ends = {{0, 1, ...},
{1, 2, ...}, {2, 3, ...}, ...}
14 Set(ends)
Split, 13
15 ALL(a):[a e ends <=> a e pn &
EXIST(b):[b e n & ALL(c):[c e a =>
b<=c]]]
Split, 13
Prove: ~EXIST(a):ALL(b):[b e ends => a e b]
Suppose to the contrary...
16 EXIST(a):ALL(b):[b e ends => a e b]
Premise
Define: x
17 ALL(b):[b e ends => x e b]
E Spec, 16
Construct y
Apply the Subset Axiom
18 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & x<a]]
Subset, 1
19 Set(y) & ALL(a):[a e y <=> a e n & x<a]
E Spec, 18
Define: y
20 Set(y)
Split, 19
21 ALL(a):[a e y <=> a e n & x<a]
Split, 19
Prove: ~x e y
Apply the definition of y
22 x e y <=> x e n & x<x
U Spec, 21
23 [x e y => x e n & x<x] & [x e n & x<x => x e y]
Iff-And, 22
24 x e y => x e n & x<x
Split, 23
25 x e n & x<x => x e y
Split, 23
26 ~[x e n & x<x] => ~x e y
Contra, 24
27 ~~[x e n => ~x<x] => ~x e y
Imply-And, 26
28 x e n => ~x<x => ~x e y
Rem DNeg, 27
29 x e n => ~x<x
U Spec, 3
As Required:
30 ~x e y
Detach, 28, 29
Sufficient: For x e y (to obtain
contradiction)
31 y e ends => x e y
U Spec, 17
Prove: y e ends
Apply definition of ends
32 y e ends <=> y e pn & EXIST(b):[b e n & ALL(c):[c e y => b<=c]]
U Spec, 15
33 [y e ends => y e pn & EXIST(b):[b e n & ALL(c):[c e y => b<=c]]]
&
[y e pn & EXIST(b):[b e n & ALL(c):[c e y => b<=c]] => y e ends]
Iff-And, 32
34 y e ends => y e pn & EXIST(b):[b e n & ALL(c):[c e y => b<=c]]
Split, 33
Sufficient: For y e ends
35 y e pn & EXIST(b):[b e n & ALL(c):[c e y => b<=c]] => y e ends
Split, 33
Prove: y e pn
Apply definition of pn
36 y e pn <=> Set(y) & ALL(d):[d e y => d e n]
U Spec, 11
37 [y e pn => Set(y) & ALL(d):[d e y => d e n]]
&
[Set(y) & ALL(d):[d e y => d e n] => y e pn]
Iff-And, 36
38 y e pn => Set(y) & ALL(d):[d e y => d e n]
Split, 37
Sufficient: For y e pn
39 Set(y) & ALL(d):[d e y => d e n] => y e pn
Split, 37
Prove: ALL(d):[d e y => d e n]
Suppose...
40 z e y
Premise
Apply definition of y
41 z e y <=> z e n & x<z
U Spec, 21
42 [z e y => z e n & x<z] & [z e n & x<z => z e y]
Iff-And, 41
43 z e y => z e n & x<z
Split, 42
44 z e n & x<z => z e y
Split, 42
45 z e n & x<z
Detach, 43, 40
46 z e n
Split, 45
As Required:
47 ALL(d):[d e y => d e n]
4 Conclusion, 40
Joining results...
48 Set(y) & ALL(d):[d e y => d e n]
Join, 20, 47
As Required:
49 y e pn
Detach, 39, 48
Prove: ALL(c):[c e y => 0<=c]
Suppose...
50 z e y
Premise
Apply definition of y
51 z e y <=> z e n & x<z
U Spec, 21
52 [z e y => z e n & x<z] & [z e n & x<z => z e y]
Iff-And, 51
53 z e y => z e n & x<z
Split, 52
54 z e n & x<z => z e y
Split, 52
55 z e n & x<z
Detach, 53, 50
56 z e n
Split, 55
57 x<z
Split, 55
Apply axiom
58 z e n => 0<=z
U Spec, 5
59 0<=z
Detach, 58, 56
As Required:
60 ALL(c):[c e y => 0<=c]
4 Conclusion, 50
Joining results...
61 0 e n & ALL(c):[c e y => 0<=c]
Join, 2, 60
62 EXIST(b):[b e n & ALL(c):[c e y => b<=c]]
E Gen, 61
63 y e pn
&
EXIST(b):[b e n & ALL(c):[c e y => b<=c]]
Join, 49, 62
64 y e ends
Detach, 35, 63
65 x e y
Detach, 31, 64
Obtain the contradiction...
66 x e y & ~x e y
Join, 65, 30
As Required:
67 ~EXIST(a):ALL(b):[b e ends => a e b]
4 Conclusion, 16