THEOREM
*******
Given:
1. Peano systems (n,next,0) and (n',next',0')
2. f: n --> n' (as defined below)
3. f': n' --> n (as defined below
Prove:
1. f' is the inverse of f, i.e. f is a bijection (lines 19 - 80)
ALL(a):[a e n => f'(f(a))=a]
2. f is injective (lines 81 - 92)
ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
3. f preserves the successor relation (lines 93 - 117)
ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]]
(This proof was written with the aid of the author's DC Proof 2.0 software available at
DEFINITIONS
**********
Peano system (n,0,next)
***********************
1 Set(n)
Axiom
2 0 e n
Axiom
next is a function on n
3 ALL(a):[a e n => next(a) e n]
Axiom
next is an injective (1-to-1) function
If x has a predecessor, that predecessor is unique.
4 ALL(a):ALL(b):[a e n & b e n => [next(a)=next(b) => a=b]]
Axiom
0 has no predecessor under next
5 ALL(a):[a e n => ~next(a)=0]
Axiom
Principle of mathematical induction (PMI) for (n,0,next)
6 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]]]
Axiom
Peano system (n',0',next')
**************************
7 Set(n')
Axiom
8 0' e n'
Axiom
next' is a function on n'
9 ALL(a):[a e n' => next'(a) e n']
Axiom
next' is an injective (1-to-1) function
10 ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
Axiom
0' has no predecessor under next'
11 ALL(a):[a e n' => ~next'(a)=0']
Axiom
Principle of mathematical induction (PMI) for (n',0',next')
12 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]]]
Axiom
Define: f (previously constructed) EquivalentPeanoSystemsA.htm
*********
13 ALL(a):[a e n => f(a) e n']
Axiom
14 f(0)=0'
Axiom
15 ALL(a):[a e n => f(next(a))=next'(f(a))]
Axiom
Define: f' (similarly to f)
**********
16 ALL(a):[a e n' => f'(a) e n]
Axiom
17 f'(0')=0
Axiom
18 ALL(a):[a e n' => f'(next'(a))=next(f'(a))]
Axiom
PROOF
*****
Prove: f' is the inverse of f by induction
Construct subset p to apply PMI
Applying Subset Axiom...
19 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & f'(f(a))=a]]
Subset, 1
20 Set(p) & ALL(a):[a e p <=> a e n & f'(f(a))=a]
E Spec, 19
Define: p
21 Set(p)
Split, 20
22 ALL(a):[a e p <=> a e n & f'(f(a))=a]
Split, 20
Apply PMI on n
23 Set(p) & ALL(b):[b e p => b e n]
=> [0 e p & ALL(b):[b e p => next(b) e p]
=> ALL(b):[b e n => b e p]]
U Spec, 6
Prove: ALL(a):[a e p => a e n]
Suppose...
24 x e p
Premise
25 x e p <=> x e n & f'(f(x))=x
U Spec, 22
26 [x e p => x e n & f'(f(x))=x]
& [x e n & f'(f(x))=x => x e p]
Iff-And, 25
27 x e p => x e n & f'(f(x))=x
Split, 26
28 x e n & f'(f(x))=x => x e p
Split, 26
29 x e n & f'(f(x))=x
Detach, 27, 24
30 x e n
Split, 29
As Required:
31 ALL(a):[a e p => a e n]
4 Conclusion, 24
32 Set(p) & ALL(a):[a e p => a e n]
Join, 21, 31
Sufficient: ALL(b):[b e n => b e p]
33 0 e p & ALL(b):[b e p => next(b) e p]
=> ALL(b):[b e n => b e p]
Detach, 23, 32
Prove: 0 e p (base case)
Apply definition of p
34 0 e p <=> 0 e n & f'(f(0))=0
U Spec, 22
35 [0 e p => 0 e n & f'(f(0))=0]
& [0 e n & f'(f(0))=0 => 0 e p]
Iff-And, 34
36 0 e p => 0 e n & f'(f(0))=0
Split, 35
Sufficient: For 0 e p
37 0 e n & f'(f(0))=0 => 0 e p
Split, 35
38 f'(f(0))=0
Substitute, 14, 17
39 0 e n & f'(f(0))=0
Join, 2, 38
As Required:
40 0 e p
Detach, 37, 39
Prove: ALL(a):[a e p => next(a) e p] (inductive case)
Suppose...
41 x e p
Premise
Apply definition of p for x
42 x e p <=> x e n & f'(f(x))=x
U Spec, 22
43 [x e p => x e n & f'(f(x))=x]
& [x e n & f'(f(x))=x => x e p]
Iff-And, 42
44 x e p => x e n & f'(f(x))=x
Split, 43
45 x e n & f'(f(x))=x => x e p
Split, 43
46 x e n & f'(f(x))=x
Detach, 44, 41
47 x e n
Split, 46
48 f'(f(x))=x
Split, 46
Apply definition of p for next(x)
49 next(x) e p <=> next(x) e n & f'(f(next(x)))=next(x)
U Spec, 22
50 [next(x) e p => next(x) e n & f'(f(next(x)))=next(x)]
& [next(x) e n & f'(f(next(x)))=next(x) => next(x) e p]
Iff-And, 49
51 next(x) e p => next(x) e n & f'(f(next(x)))=next(x)
Split, 50
Sufficient: For next(x) e p
52 next(x) e n & f'(f(next(x)))=next(x) => next(x) e p
Split, 50
Prove: next(x) e n
53 x e n => next(x) e n
U Spec, 3
As Required:
54 next(x) e n
Detach, 53, 47
Prove: f'(f(next(x)))=next(x)
55 f'(f(next(x)))=f'(f(next(x)))
Reflex
56 x e n => f(next(x))=next'(f(x))
U Spec, 15
57 f(next(x))=next'(f(x))
Detach, 56, 47
58 f'(f(next(x)))=f'(next'(f(x)))
Substitute, 57, 55
59 f(x) e n' => f'(next'(f(x)))=next(f'(f(x)))
U Spec, 18
60 x e n => f(x) e n'
U Spec, 13
61 f(x) e n'
Detach, 60, 47
62 f'(next'(f(x)))=next(f'(f(x)))
Detach, 59, 61
63 f'(f(next(x)))=next(f'(f(x)))
Substitute, 62, 58
As Required:
64 f'(f(next(x)))=next(x)
Substitute, 48, 63
65 next(x) e n & f'(f(next(x)))=next(x)
Join, 54, 64
66 next(x) e p
Detach, 52, 65
As Required:
67 ALL(a):[a e p => next(a) e p]
4 Conclusion, 41
68 0 e p & ALL(a):[a e p => next(a) e p]
Join, 40, 67
As Required:
69 ALL(b):[b e n => b e p]
Detach, 33, 68
Prove: ALL(a):[a e n => f'(f(a))=a]
Suppose...
70 x e n
Premise
71 x e n => x e p
U Spec, 69
72 x e p
Detach, 71, 70
73 x e p <=> x e n & f'(f(x))=x
U Spec, 22
74 [x e p => x e n & f'(f(x))=x]
& [x e n & f'(f(x))=x => x e p]
Iff-And, 73
75 x e p => x e n & f'(f(x))=x
Split, 74
76 x e n & f'(f(x))=x => x e p
Split, 74
77 x e n & f'(f(x))=x
Detach, 75, 72
78 x e n
Split, 77
79 f'(f(x))=x
Split, 77
f' is the inverse of f (f is a bijection)
As Required:
80 ALL(a):[a e n => f'(f(a))=a]
4 Conclusion, 70
Prove: f is injective
Suppose...
81 x e n & y e n
Premise
82 x e n
Split, 81
83 y e n
Split, 81
Prove: f(x)=f(y) => x=y
Suppose...
84 f(x)=f(y)
Premise
85 x e n => f'(f(x))=x
U Spec, 80
86 f'(f(x))=x
Detach, 85, 82
87 f'(f(y))=x
Substitute, 84, 86
88 y e n => f'(f(y))=y
U Spec, 80
89 f'(f(y))=y
Detach, 88, 83
90 x=y
Substitute, 87, 89
As Required:
91 f(x)=f(y) => x=y
4 Conclusion, 84
f is injective
As Required:
92 ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
4 Conclusion, 81
Prove: f preserves successor relation
Suppose...
93 x e n & y e n
Premise
94 x e n
Split, 93
95 y e n
Split, 93
'=>'
Prove: next(x)=y => next'(f(x))=f(y)
Suppose...
96 next(x)=y
Premise
97 next'(f(x))=next'(f(x))
Reflex
98 x e n => f(next(x))=next'(f(x))
U Spec, 15
99 f(next(x))=next'(f(x))
Detach, 98, 94
100 next'(f(x))=f(next(x))
Substitute, 99, 97
101 next'(f(x))=f(y)
Substitute, 96, 100
As Required:
102 next(x)=y => next'(f(x))=f(y)
4 Conclusion, 96
'<='
Prove: next'(f(x))=f(y) => next(x)=y
Suppose...
103 next'(f(x))=f(y)
Premise
104 x e n => f(next(x))=next'(f(x))
U Spec, 15
105 f(next(x))=next'(f(x))
Detach, 104, 94
106 f(next(x))=f(y)
Substitute, 105, 103
Apply injectivity of f
107 ALL(b):[next(x) e n & b e n => [f(next(x))=f(b) => next(x)=b]]
U Spec, 92
108 next(x) e n & y e n => [f(next(x))=f(y) => next(x)=y]
U Spec, 107
109 x e n => next(x) e n
U Spec, 3
110 next(x) e n
Detach, 109, 94
111 next(x) e n & y e n
Join, 110, 95
112 f(next(x))=f(y) => next(x)=y
Detach, 108, 111
113 next(x)=y
Detach, 112, 106
As Required:
114 next'(f(x))=f(y) => next(x)=y
4 Conclusion, 103
115 [next(x)=y => next'(f(x))=f(y)]
& [next'(f(x))=f(y) => next(x)=y]
Join, 102, 114
116 next(x)=y <=> next'(f(x))=f(y)
Iff-And, 115
f preserves successor relation
As Required:
117 ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]]
4 Conclusion, 93