THEOREM 2
*********
The unique mapping between a pair of Peano systems (n,0,next) and (n',0,next') is a bijection.
Outline
*******
Line 1 Previous result (Theorem 1)
Lines 2 - 4 Initial assumptions
Lines 5 - 41 Apply Theorem 1
Lines 42 - 103 Prove by induction that f' is the inverse of f
Lines 105 - 115 Prove by induction that f is injective
Lines 116 - 177 Prove by induction that f is the inverse of f'
Lines 178 - 185 Prove f is surjective
Lines 186 - 188 Generalizing
This proof was written with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com
PREVIOUS RESULT
***************
From Theorem 1, the exists a unique mapping between Peano systems (n,0,next) and (n',0',next')
1 ALL(n1):ALL(z1):ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(n1)
& z1 e n1
& ALL(a):[a e n1 => next1(a) e n1]
& ALL(a):ALL(b):[a e n1 & b e n1 => [next1(a)=next1(b) => a=b]]
& ALL(a):[a e n1 => ~next1(a)=z1]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n1]
=> [z1 e a & ALL(b):[b e a => next1(b) e a]
=> ALL(b):[b e n1 => b e a]]]
& Set(n2)
& z2 e n2
& ALL(a):[a e n2 => next2(a) e n2]
& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n2 => ~next2(a)=z2]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n2]
=> [z2 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n2 => b e a]]]
=> EXIST(f1):[ALL(a):[a e n1 => f1(a) e n2] & f1(z1)=z2
& ALL(a):[a e n1 => f1(next1(a))=next2(f1(a))]
& ALL(f2):[ALL(a):[a e n1 => f2(a) e n2]
& f2(z1)=z2
& ALL(a):[a e n1 => f2(next1(a))=next2(f2(a))]
=> ALL(a):[a e n1 => f2(a)=f1(a)]]]]
Axiom
PROOF
*****
Suppose...
2 Set(n)
& 0 e n
& ALL(a):[a e n => next(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [next(a)=next(b) => a=b]]
& ALL(a):[a e n => ~next(a)=0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a => next(b) e a]
=> ALL(b):[b e n => b e a]]]
& Set(n')
& 0' e n'
& ALL(a):[a e n' => next'(a) e n']
& ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
& ALL(a):[a e n' => ~next'(a)=0']
& ALL(a):[Set(a) & ALL(b):[b e a => b e n']
=> [0' e a & ALL(b):[b e a => next'(b) e a]
=> ALL(b):[b e n' => b e a]]]
Premise
Peano's Axioms (n,0,next)
**************
3 Set(n)
Split, 2
4 0 e n
Split, 2
5 ALL(a):[a e n => next(a) e n]
Split, 2
6 ALL(a):ALL(b):[a e n & b e n => [next(a)=next(b) => a=b]]
Split, 2
7 ALL(a):[a e n => ~next(a)=0]
Split, 2
8 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a => next(b) e a]
=> ALL(b):[b e n => b e a]]]
Split, 2
Peano's Axioms (n',0',next')
**************
9 Set(n')
Split, 2
10 0' e n'
Split, 2
11 ALL(a):[a e n' => next'(a) e n']
Split, 2
12 ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
Split, 2
13 ALL(a):[a e n' => ~next'(a)=0']
Split, 2
14 ALL(a):[Set(a) & ALL(b):[b e a => b e n']
=> [0' e a & ALL(b):[b e a => next'(b) e a]
=> ALL(b):[b e n' => b e a]]]
Split, 2
Prove: ALL(f):[ALL(a):[a e n => f(a) e n']
& f(0)=0'
& ALL(a):[a e n => f(next(a))=next'(f(a))]
=> ALL(a):[a e n' => EXIST(b):[b e n & f(b)=a]] <--- f is surjective
& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]] <--- f in injective
Suppose...
15 ALL(a):[a e n => f(a) e n']
& f(0)=0'
& ALL(a):[a e n => f(next(a))=next'(f(a))]
Premise
16 ALL(a):[a e n => f(a) e n']
Split, 15
17 f(0)=0'
Split, 15
18 ALL(a):[a e n => f(next(a))=next'(f(a))]
Split, 15
Apply previous result
19 ALL(z1):ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(n')
& z1 e n'
& ALL(a):[a e n' => next1(a) e n']
& ALL(a):ALL(b):[a e n' & b e n' => [next1(a)=next1(b) => a=b]]
& ALL(a):[a e n' => ~next1(a)=z1]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n']
=> [z1 e a & ALL(b):[b e a => next1(b) e a]
=> ALL(b):[b e n' => b e a]]]
& Set(n2)
& z2 e n2
& ALL(a):[a e n2 => next2(a) e n2]
& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n2 => ~next2(a)=z2]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n2]
=> [z2 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n2 => b e a]]]
=> EXIST(f1):[ALL(a):[a e n' => f1(a) e n2] & f1(z1)=z2
& ALL(a):[a e n' => f1(next1(a))=next2(f1(a))]
& ALL(f2):[ALL(a):[a e n' => f2(a) e n2]
& f2(z1)=z2
& ALL(a):[a e n' => f2(next1(a))=next2(f2(a))]
=> ALL(a):[a e n' => f2(a)=f1(a)]]]]
U Spec, 1
20 ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(n')
& 0' e n'
& ALL(a):[a e n' => next1(a) e n']
& ALL(a):ALL(b):[a e n' & b e n' => [next1(a)=next1(b) => a=b]]
& ALL(a):[a e n' => ~next1(a)=0']
& ALL(a):[Set(a) & ALL(b):[b e a => b e n']
=> [0' e a & ALL(b):[b e a => next1(b) e a]
=> ALL(b):[b e n' => b e a]]]
& Set(n2)
& z2 e n2
& ALL(a):[a e n2 => next2(a) e n2]
& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n2 => ~next2(a)=z2]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n2]
=> [z2 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n2 => b e a]]]
=> EXIST(f1):[ALL(a):[a e n' => f1(a) e n2] & f1(0')=z2
& ALL(a):[a e n' => f1(next1(a))=next2(f1(a))]
& ALL(f2):[ALL(a):[a e n' => f2(a) e n2]
& f2(0')=z2
& ALL(a):[a e n' => f2(next1(a))=next2(f2(a))]
=> ALL(a):[a e n' => f2(a)=f1(a)]]]]
U Spec, 19
21 ALL(n2):ALL(z2):ALL(next2):[Set(n')
& 0' e n'
& ALL(a):[a e n' => next'(a) e n']
& ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
& ALL(a):[a e n' => ~next'(a)=0']
& ALL(a):[Set(a) & ALL(b):[b e a => b e n']
=> [0' e a & ALL(b):[b e a => next'(b) e a]
=> ALL(b):[b e n' => b e a]]]
& Set(n2)
& z2 e n2
& ALL(a):[a e n2 => next2(a) e n2]
& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n2 => ~next2(a)=z2]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n2]
=> [z2 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n2 => b e a]]]
=> EXIST(f1):[ALL(a):[a e n' => f1(a) e n2] & f1(0')=z2
& ALL(a):[a e n' => f1(next'(a))=next2(f1(a))]
& ALL(f2):[ALL(a):[a e n' => f2(a) e n2]
& f2(0')=z2
& ALL(a):[a e n' => f2(next'(a))=next2(f2(a))]
=> ALL(a):[a e n' => f2(a)=f1(a)]]]]
U Spec, 20
22 ALL(z2):ALL(next2):[Set(n')
& 0' e n'
& ALL(a):[a e n' => next'(a) e n']
& ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
& ALL(a):[a e n' => ~next'(a)=0']
& ALL(a):[Set(a) & ALL(b):[b e a => b e n']
=> [0' e a & ALL(b):[b e a => next'(b) e a]
=> ALL(b):[b e n' => b e a]]]
& Set(n)
& z2 e n
& ALL(a):[a e n => next2(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n => ~next2(a)=z2]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [z2 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n => b e a]]]
=> EXIST(f1):[ALL(a):[a e n' => f1(a) e n] & f1(0')=z2
& ALL(a):[a e n' => f1(next'(a))=next2(f1(a))]
& ALL(f2):[ALL(a):[a e n' => f2(a) e n]
& f2(0')=z2
& ALL(a):[a e n' => f2(next'(a))=next2(f2(a))]
=> ALL(a):[a e n' => f2(a)=f1(a)]]]]
U Spec, 21
23 ALL(next2):[Set(n')
& 0' e n'
& ALL(a):[a e n' => next'(a) e n']
& ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
& ALL(a):[a e n' => ~next'(a)=0']
& ALL(a):[Set(a) & ALL(b):[b e a => b e n']
=> [0' e a & ALL(b):[b e a => next'(b) e a]
=> ALL(b):[b e n' => b e a]]]
& Set(n)
& 0 e n
& ALL(a):[a e n => next2(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n => ~next2(a)=0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n => b e a]]]
=> EXIST(f1):[ALL(a):[a e n' => f1(a) e n] & f1(0')=0
& ALL(a):[a e n' => f1(next'(a))=next2(f1(a))]
& ALL(f2):[ALL(a):[a e n' => f2(a) e n]
& f2(0')=0
& ALL(a):[a e n' => f2(next'(a))=next2(f2(a))]
=> ALL(a):[a e n' => f2(a)=f1(a)]]]]
U Spec, 22
24 Set(n')
& 0' e n'
& ALL(a):[a e n' => next'(a) e n']
& ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
& ALL(a):[a e n' => ~next'(a)=0']
& ALL(a):[Set(a) & ALL(b):[b e a => b e n']
=> [0' e a & ALL(b):[b e a => next'(b) e a]
=> ALL(b):[b e n' => b e a]]]
& Set(n)
& 0 e n
& ALL(a):[a e n => next(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [next(a)=next(b) => a=b]]
& ALL(a):[a e n => ~next(a)=0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a => next(b) e a]
=> ALL(b):[b e n => b e a]]]
=> EXIST(f1):[ALL(a):[a e n' => f1(a) e n] & f1(0')=0
& ALL(a):[a e n' => f1(next'(a))=next(f1(a))]
& ALL(f2):[ALL(a):[a e n' => f2(a) e n]
& f2(0')=0
& ALL(a):[a e n' => f2(next'(a))=next(f2(a))]
=> ALL(a):[a e n' => f2(a)=f1(a)]]]
U Spec, 23
25 Set(n') & 0' e n'
Join, 9, 10
26 Set(n') & 0' e n'
& ALL(a):[a e n' => next'(a) e n']
Join, 25, 11
27 Set(n') & 0' e n'
& ALL(a):[a e n' => next'(a) e n']
& ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
Join, 26, 12
28 Set(n') & 0' e n'
& ALL(a):[a e n' => next'(a) e n']
& ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
& ALL(a):[a e n' => ~next'(a)=0']
Join, 27, 13
29 Set(n') & 0' e n'
& ALL(a):[a e n' => next'(a) e n']
& ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
& ALL(a):[a e n' => ~next'(a)=0']
& ALL(a):[Set(a) & ALL(b):[b e a => b e n']
=> [0' e a & ALL(b):[b e a => next'(b) e a]
=> ALL(b):[b e n' => b e a]]]
Join, 28, 14
30 Set(n') & 0' e n'
& ALL(a):[a e n' => next'(a) e n']
& ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
& ALL(a):[a e n' => ~next'(a)=0']
& ALL(a):[Set(a) & ALL(b):[b e a => b e n']
=> [0' e a & ALL(b):[b e a => next'(b) e a]
=> ALL(b):[b e n' => b e a]]]
& Set(n)
Join, 29, 3
31 Set(n') & 0' e n'
& ALL(a):[a e n' => next'(a) e n']
& ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
& ALL(a):[a e n' => ~next'(a)=0']
& ALL(a):[Set(a) & ALL(b):[b e a => b e n']
=> [0' e a & ALL(b):[b e a => next'(b) e a]
=> ALL(b):[b e n' => b e a]]]
& Set(n)
& 0 e n
Join, 30, 4
32 Set(n') & 0' e n'
& ALL(a):[a e n' => next'(a) e n']
& ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
& ALL(a):[a e n' => ~next'(a)=0']
& ALL(a):[Set(a) & ALL(b):[b e a => b e n']
=> [0' e a & ALL(b):[b e a => next'(b) e a]
=> ALL(b):[b e n' => b e a]]]
& Set(n)
& 0 e n
& ALL(a):[a e n => next(a) e n]
Join, 31, 5
33 Set(n') & 0' e n'
& ALL(a):[a e n' => next'(a) e n']
& ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
& ALL(a):[a e n' => ~next'(a)=0']
& ALL(a):[Set(a) & ALL(b):[b e a => b e n']
=> [0' e a & ALL(b):[b e a => next'(b) e a]
=> ALL(b):[b e n' => b e a]]]
& Set(n)
& 0 e n
& ALL(a):[a e n => next(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [next(a)=next(b) => a=b]]
Join, 32, 6
34 Set(n') & 0' e n'
& ALL(a):[a e n' => next'(a) e n']
& ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
& ALL(a):[a e n' => ~next'(a)=0']
& ALL(a):[Set(a) & ALL(b):[b e a => b e n']
=> [0' e a & ALL(b):[b e a => next'(b) e a]
=> ALL(b):[b e n' => b e a]]]
& Set(n)
& 0 e n
& ALL(a):[a e n => next(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [next(a)=next(b) => a=b]]
& ALL(a):[a e n => ~next(a)=0]
Join, 33, 7
35 Set(n') & 0' e n'
& ALL(a):[a e n' => next'(a) e n']
& ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
& ALL(a):[a e n' => ~next'(a)=0']
& ALL(a):[Set(a) & ALL(b):[b e a => b e n']
=> [0' e a & ALL(b):[b e a => next'(b) e a]
=> ALL(b):[b e n' => b e a]]]
& Set(n)
& 0 e n
& ALL(a):[a e n => next(a) e n]
& ALL(a):ALL(b):[a e n & b e n => [next(a)=next(b) => a=b]]
& ALL(a):[a e n => ~next(a)=0]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a => next(b) e a]
=> ALL(b):[b e n => b e a]]]
Join, 34, 8
36 EXIST(f1):[ALL(a):[a e n' => f1(a) e n] & f1(0')=0
& ALL(a):[a e n' => f1(next'(a))=next(f1(a))]
& ALL(f2):[ALL(a):[a e n' => f2(a) e n]
& f2(0')=0
& ALL(a):[a e n' => f2(next'(a))=next(f2(a))]
=> ALL(a):[a e n' => f2(a)=f1(a)]]]
Detach, 24, 35
37 ALL(a):[a e n' => f'(a) e n] & f'(0')=0
& ALL(a):[a e n' => f'(next'(a))=next(f'(a))]
& ALL(f2):[ALL(a):[a e n' => f2(a) e n]
& f2(0')=0
& ALL(a):[a e n' => f2(next'(a))=next(f2(a))]
=> ALL(a):[a e n' => f2(a)=f'(a)]]
E Spec, 36
Define: f'
38 ALL(a):[a e n' => f'(a) e n]
Split, 37
39 f'(0')=0
Split, 37
40 ALL(a):[a e n' => f'(next'(a))=next(f'(a))]
Split, 37
41 ALL(f2):[ALL(a):[a e n' => f2(a) e n]
& f2(0')=0
& ALL(a):[a e n' => f2(next'(a))=next(f2(a))]
=> ALL(a):[a e n' => f2(a)=f'(a)]]
Split, 37
Prove by induction that f' is the inverse of f
Apply Subset Axiom
42 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & f'(f(a))=a]]
Subset, 3
43 Set(p1) & ALL(a):[a e p1 <=> a e n & f'(f(a))=a]
E Spec, 42
Define: p1
44 Set(p1)
Split, 43
45 ALL(a):[a e p1 <=> a e n & f'(f(a))=a]
Split, 43
Apply PMI for n
46 Set(p1) & ALL(b):[b e p1 => b e n]
=> [0 e p1 & ALL(b):[b e p1 => next(b) e p1]
=> ALL(b):[b e n => b e p1]]
U Spec, 8
Prove: ALL(a):[a e p1 => a e n]
Suppose...
47 x e p1
Premise
Apply definition of p1
48 x e p1 <=> x e n & f'(f(x))=x
U Spec, 45
49 [x e p1 => x e n & f'(f(x))=x]
& [x e n & f'(f(x))=x => x e p1]
Iff-And, 48
50 x e p1 => x e n & f'(f(x))=x
Split, 49
51 x e n & f'(f(x))=x => x e p1
Split, 49
52 x e n & f'(f(x))=x
Detach, 50, 47
53 x e n
Split, 52
As Required:
54 ALL(a):[a e p1 => a e n]
4 Conclusion, 47
55 Set(p1) & ALL(a):[a e p1 => a e n]
Join, 44, 54
Sufficient: ALL(a):[a e p1 => a e n]
56 0 e p1 & ALL(b):[b e p1 => next(b) e p1]
=> ALL(b):[b e n => b e p1]
Detach, 46, 55
BASE CASE
*********
57 0 e p1 <=> 0 e n & f'(f(0))=0
U Spec, 45
58 [0 e p1 => 0 e n & f'(f(0))=0]
& [0 e n & f'(f(0))=0 => 0 e p1]
Iff-And, 57
59 0 e p1 => 0 e n & f'(f(0))=0
Split, 58
Sufficient: 0 e p1
60 0 e n & f'(f(0))=0 => 0 e p1
Split, 58
61 0 e n & f'(0')=0 => 0 e p1
Substitute, 17, 60
62 0 e n & f'(0')=0
Join, 4, 39
As Required:
63 0 e p1
Detach, 61, 62
INDUCTIVE STEP
**************
Prove: ALL(a):[a e p1 => next(a) e p1]
Suppose...
64 x e p1
Premise
Apply definition of p1
65 x e p1 <=> x e n & f'(f(x))=x
U Spec, 45
66 [x e p1 => x e n & f'(f(x))=x]
& [x e n & f'(f(x))=x => x e p1]
Iff-And, 65
67 x e p1 => x e n & f'(f(x))=x
Split, 66
68 x e n & f'(f(x))=x => x e p1
Split, 66
69 x e n & f'(f(x))=x
Detach, 67, 64
70 x e n
Split, 69
71 f'(f(x))=x
Split, 69
Apply definition of p1
72 next(x) e p1 <=> next(x) e n & f'(f(next(x)))=next(x)
U Spec, 45
73 [next(x) e p1 => next(x) e n & f'(f(next(x)))=next(x)]
& [next(x) e n & f'(f(next(x)))=next(x) => next(x) e p1]
Iff-And, 72
74 next(x) e p1 => next(x) e n & f'(f(next(x)))=next(x)
Split, 73
Sufficient: next(x) e p1
75 next(x) e n & f'(f(next(x)))=next(x) => next(x) e p1
Split, 73
76 x e n => next(x) e n
U Spec, 5
77 next(x) e n
Detach, 76, 70
78 f'(f(next(x)))=f'(f(next(x)))
Reflex
79 x e n => f(next(x))=next'(f(x))
U Spec, 18
80 f(next(x))=next'(f(x))
Detach, 79, 70
81 f'(f(next(x)))=f'(next'(f(x)))
Substitute, 80, 78
82 f(x) e n' => f'(next'(f(x)))=next(f'(f(x)))
U Spec, 40
83 x e n => f(x) e n'
U Spec, 16
84 f(x) e n'
Detach, 83, 70
85 f'(next'(f(x)))=next(f'(f(x)))
Detach, 82, 84
86 f'(f(next(x)))=next(f'(f(x)))
Substitute, 85, 81
87 f'(f(next(x)))=next(x)
Substitute, 71, 86
88 next(x) e n & f'(f(next(x)))=next(x)
Join, 77, 87
89 next(x) e p1
Detach, 75, 88
As Required:
90 ALL(a):[a e p1 => next(a) e p1]
4 Conclusion, 64
91 0 e p1 & ALL(a):[a e p1 => next(a) e p1]
Join, 63, 90
92 ALL(b):[b e n => b e p1]
Detach, 56, 91
Prove: ALL(a):[a e n => f'(f(a))=a]
Suppose...
93 x e n
Premise
94 x e n => x e p1
U Spec, 92
95 x e p1
Detach, 94, 93
Apply definition of p1
96 x e p1 <=> x e n & f'(f(x))=x
U Spec, 45
97 [x e p1 => x e n & f'(f(x))=x]
& [x e n & f'(f(x))=x => x e p1]
Iff-And, 96
98 x e p1 => x e n & f'(f(x))=x
Split, 97
99 x e n & f'(f(x))=x => x e p1
Split, 97
100 x e n & f'(f(x))=x
Detach, 98, 95
101 x e n
Split, 100
102 f'(f(x))=x
Split, 100
As Required:
103 ALL(a):[a e n => f'(f(a))=a]
4 Conclusion, 93
Prove: ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]] (f is injective)
Suppose...
104 x e n & y e n
Premise
105 x e n
Split, 104
106 y e n
Split, 104
Prove: f(x)=f(y) => x=y
Suppose...
107 f(x)=f(y)
Premise
Apply previous result
108 x e n => f'(f(x))=x
U Spec, 103
109 f'(f(x))=x
Detach, 108, 105
110 f'(f(y))=x
Substitute, 107, 109
111 y e n => f'(f(y))=y
U Spec, 103
112 f'(f(y))=y
Detach, 111, 106
113 x=y
Substitute, 110, 112
As Required:
114 f(x)=f(y) => x=y
4 Conclusion, 107
f is injective
As Required:
115 ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
4 Conclusion, 104
Prove by induction that f is the inverse of f'
Apply Subset Axiom
116 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n' & f(f'(a))=a]]
Subset, 9
117 Set(p2) & ALL(a):[a e p2 <=> a e n' & f(f'(a))=a]
E Spec, 116
Define: p2
118 Set(p2)
Split, 117
119 ALL(a):[a e p2 <=> a e n' & f(f'(a))=a]
Split, 117
Apply PMI on n'
120 Set(p2) & ALL(b):[b e p2 => b e n']
=> [0' e p2 & ALL(b):[b e p2 => next'(b) e p2]
=> ALL(b):[b e n' => b e p2]]
U Spec, 14
Prove: ALL(a):[a e p2 => a e n']
Suppose...
121 x e p2
Premise
Apply definition of p2
122 x e p2 <=> x e n' & f(f'(x))=x
U Spec, 119
123 [x e p2 => x e n' & f(f'(x))=x]
& [x e n' & f(f'(x))=x => x e p2]
Iff-And, 122
124 x e p2 => x e n' & f(f'(x))=x
Split, 123
125 x e n' & f(f'(x))=x => x e p2
Split, 123
126 x e n' & f(f'(x))=x
Detach, 124, 121
127 x e n'
Split, 126
As Required:
128 ALL(a):[a e p2 => a e n']
4 Conclusion, 121
129 Set(p2) & ALL(a):[a e p2 => a e n']
Join, 118, 128
Sufficient: For ALL(b):[b e n' => b e p2]
130 0' e p2 & ALL(b):[b e p2 => next'(b) e p2]
=> ALL(b):[b e n' => b e p2]
Detach, 120, 129
BASE CASE
*********
Prove 0' e p2
Apply definition of p2
131 0' e p2 <=> 0' e n' & f(f'(0'))=0'
U Spec, 119
132 [0' e p2 => 0' e n' & f(f'(0'))=0']
& [0' e n' & f(f'(0'))=0' => 0' e p2]
Iff-And, 131
133 0' e p2 => 0' e n' & f(f'(0'))=0'
Split, 132
Sufficient: For 0' e p2
134 0' e n' & f(f'(0'))=0' => 0' e p2
Split, 132
135 f(f'(0'))=0'
Substitute, 39, 17
136 0' e n' & f(f'(0'))=0'
Join, 10, 135
As Required:
137 0' e p2
Detach, 134, 136
INDUCTIVE STEP
**************
Prove: ALL(a):[a e p2 => next'(a) e p2]
Suppose...
138 x e p2
Premise
Apply definition of p2
139 x e p2 <=> x e n' & f(f'(x))=x
U Spec, 119
140 [x e p2 => x e n' & f(f'(x))=x]
& [x e n' & f(f'(x))=x => x e p2]
Iff-And, 139
141 x e p2 => x e n' & f(f'(x))=x
Split, 140
142 x e n' & f(f'(x))=x => x e p2
Split, 140
143 x e n' & f(f'(x))=x
Detach, 141, 138
144 x e n'
Split, 143
145 f(f'(x))=x
Split, 143
Apply definition of p2
146 next'(x) e p2 <=> next'(x) e n' & f(f'(next'(x)))=next'(x)
U Spec, 119
147 [next'(x) e p2 => next'(x) e n' & f(f'(next'(x)))=next'(x)]
& [next'(x) e n' & f(f'(next'(x)))=next'(x) => next'(x) e p2]
Iff-And, 146
148 next'(x) e p2 => next'(x) e n' & f(f'(next'(x)))=next'(x)
Split, 147
Sufficient: For next'(x) e p2
149 next'(x) e n' & f(f'(next'(x)))=next'(x) => next'(x) e p2
Split, 147
150 x e n' => next'(x) e n'
U Spec, 11
151 next'(x) e n'
Detach, 150, 144
152 f(f'(next'(x)))=f(f'(next'(x)))
Reflex
153 x e n' => f'(next'(x))=next(f'(x))
U Spec, 40
154 f'(next'(x))=next(f'(x))
Detach, 153, 144
155 f(f'(next'(x)))=f(next(f'(x)))
Substitute, 154, 152
156 f'(x) e n => f(next(f'(x)))=next'(f(f'(x)))
U Spec, 18
157 x e n' => f'(x) e n
U Spec, 38
158 f'(x) e n
Detach, 157, 144
159 f(next(f'(x)))=next'(f(f'(x)))
Detach, 156, 158
160 f(f'(next'(x)))=next'(f(f'(x)))
Substitute, 159, 155
161 f(f'(next'(x)))=next'(x)
Substitute, 145, 160
162 next'(x) e n' & f(f'(next'(x)))=next'(x)
Join, 151, 161
163 next'(x) e p2
Detach, 149, 162
As Required:
164 ALL(a):[a e p2 => next'(a) e p2]
4 Conclusion, 138
165 0' e p2 & ALL(a):[a e p2 => next'(a) e p2]
Join, 137, 164
166 ALL(b):[b e n' => b e p2]
Detach, 130, 165
Prove: ALL(a):[a e n' => f(f'(a))=a]
Suppose...
167 x e n'
Premise
168 x e n' => x e p2
U Spec, 166
169 x e p2
Detach, 168, 167
Apply definition of p2
170 x e p2 <=> x e n' & f(f'(x))=x
U Spec, 119
171 [x e p2 => x e n' & f(f'(x))=x]
& [x e n' & f(f'(x))=x => x e p2]
Iff-And, 170
172 x e p2 => x e n' & f(f'(x))=x
Split, 171
173 x e n' & f(f'(x))=x => x e p2
Split, 171
174 x e n' & f(f'(x))=x
Detach, 172, 169
175 x e n'
Split, 174
176 f(f'(x))=x
Split, 174
As Required:
177 ALL(a):[a e n' => f(f'(a))=a]
4 Conclusion, 167
Prove: ALL(a):[a e n' => EXIST(b):[b e n & f(b)=a]]
Suppose...
178 y e n'
Premise
179 y e n' => f'(y) e n
U Spec, 38
180 f'(y) e n
Detach, 179, 178
181 y e n' => f(f'(y))=y
U Spec, 177
182 f(f'(y))=y
Detach, 181, 178
183 f'(y) e n & f(f'(y))=y
Join, 180, 182
184 EXIST(b):[b e n & f(b)=y]
E Gen, 183
f is surjective
As Required:
185 ALL(a):[a e n' => EXIST(b):[b e n & f(b)=a]]
4 Conclusion, 178
186 ALL(a):[a e n' => EXIST(b):[b e n & f(b)=a]]
& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
Join, 185, 115
As Required:
187 ALL(f):[ALL(a):[a e n => f(a) e n']
& f(0)=0'
& ALL(a):[a e n => f(next(a))=next'(f(a))]
=> ALL(a):[a e n' => EXIST(b):[b e n & f(b)=a]]
& ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]]
4 Conclusion, 15
As Required:
188 ALL(n1):ALL(z1):ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(n1)
& z1 e n1
& ALL(a):[a e n1 => next1(a) e n1]
& ALL(a):ALL(b):[a e n1 & b e n1 => [next1(a)=next1(b) => a=b]]
& ALL(a):[a e n1 => ~next1(a)=z1]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n1]
=> [z1 e a & ALL(b):[b e a => next1(b) e a]
=> ALL(b):[b e n1 => b e a]]]
& Set(n2)
& z2 e n2
& ALL(a):[a e n2 => next2(a) e n2]
& ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]
& ALL(a):[a e n2 => ~next2(a)=z2]
& ALL(a):[Set(a) & ALL(b):[b e a => b e n2]
=> [z2 e a & ALL(b):[b e a => next2(b) e a]
=> ALL(b):[b e n2 => b e a]]]
=> ALL(f):[ALL(a):[a e n1 => f(a) e n2]
& f(z1)=z2
& ALL(a):[a e n1 => f(next1(a))=next2(f(a))]
=> ALL(a):[a e n2 => EXIST(b):[b e n1 & f(b)=a]]
& ALL(a):ALL(b):[a e n1 & b e n1 => [f(a)=f(b) => a=b]]]]
4 Conclusion, 2