THEOREM
*******
Here we construct, i.e. prove the existence of an addition function (+) on the set of natural numbers n using Peano's Axioms, the Subset, Cartesian Product, Power Set and Function axioms (DC Proof).
Prove: EXIST(add):[ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
& ALL(a):[a e n => add(a,1)=s(a)]
& ALL(a):ALL(b):[a e n & b e n => add(a,s(b))=s(add(a,b))]]
In subsequent proofs, we will use the more standard infix '+' notation.
This proof was written and verified with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com
OUTLINE OF PROOF
****************
We begin by constructing the set all ordered triples of natural numbers (n3), as well as its power set (pn3) using the Cartesian Product and Power Set axioms (lines 1-22).
Using the Subset axiom (DC Proof), we then (lines 23-26) construct the subset of n3 (add) such that:
ALL(a):ALL(b):ALL(c):[(a,b,c) e add
<=> (a,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (a,b,c) e d]]
We then (lines 27-724) establish the functionality and other required properties of add.
PEANO'S AXIOMS
**************
1 Set(n)
Axiom
2 1 e n
Axiom
3 ALL(a):[a e n => s(a) e n]
Axiom
4 ALL(a):ALL(b):[a e n & b e n => [s(a)=s(b) => a=b]]
Axiom
5 ALL(a):[a e n => ~s(a)=1]
Axiom
6 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [1 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
Axiom
PROOF
*****
Apply Cartesian Product axiom
7
ALL(a1):ALL(a2):ALL(a3):[Set(a1) & Set(a2) & Set(a3) => EXIST(b):[Set''(b)
& ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)
e b <=> c1
e a1 & c2
e a2 & c3
e a3]]]
Cart Prod
8
ALL(a2):ALL(a3):[Set(n)
& Set(a2) & Set(a3) => EXIST(b):[Set''(b)
& ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)
e b <=> c1
e n
& c2 e
a2 & c3
e a3]]]
U Spec, 7
9
ALL(a3):[Set(n)
& Set(n)
& Set(a3) => EXIST(b):[Set''(b)
& ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)
e b <=> c1
e n
& c2 e
n
& c3 e
a3]]]
U Spec, 8
10
Set(n)
& Set(n)
& Set(n)
=> EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)
e b
<=> c1
e n
& c2 e
n
& c3 e
n]]
U Spec, 9
11 Set(n) & Set(n)
Join, 1, 1
12 Set(n) & Set(n) & Set(n)
Join, 11, 1
13 EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e n]]
Detach, 10, 12
14 Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
E Spec, 13
Define: n3
**********
The set of ordered triples of natural numbers
15 Set''(n3)
Split, 14
16 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
Split, 14
Apply Power Set axiom
17 ALL(a):[Set''(a) => EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e a]]]]
Power Set
18 Set''(n3) => EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]]
U Spec, 17
19 EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]]
Detach, 18, 15
20 Set(pn3)
& ALL(c):[c e pn3 <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]
E Spec, 19
Define: pn3
***********
The power set of n3
21 Set(pn3)
Split, 20
22 ALL(c):[c e pn3 <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]
Split, 20
Apply Subset axiom
23 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=> (a,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (a,b,c) e d]]]
Subset, 15
24 Set''(add) & ALL(a):ALL(b):ALL(c):[(a,b,c) e add
<=> (a,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (a,b,c) e d]]
E Spec, 23
Define: add
***********
25 Set''(add)
Split, 24
26 ALL(a):ALL(b):ALL(c):[(a,b,c) e add
<=> (a,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (a,b,c) e d]]
Split, 24
Prove: ALL(a):[a e n => (a,1,s(a)) e add]
Suppose...
27 x e n
Premise
28 ALL(b):ALL(c):[(x,b,c) e add
<=> (x,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,b,c) e d]]
U Spec, 26
29 ALL(c):[(x,1,c) e add
<=> (x,1,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,c) e d]]
U Spec, 28
30 (x,1,s(x)) e add
<=> (x,1,s(x)) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,s(x)) e d]
U Spec, 29
31 [(x,1,s(x)) e add => (x,1,s(x)) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,s(x)) e d]]
& [(x,1,s(x)) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,s(x)) e d] => (x,1,s(x)) e add]
Iff-And, 30
32 (x,1,s(x)) e add => (x,1,s(x)) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,s(x)) e d]
Split, 31
Sufficient: For (x,1,s(x)) e add
33 (x,1,s(x)) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,s(x)) e d] => (x,1,s(x)) e add
Split, 31
34 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 16
35 ALL(c3):[(x,1,c3) e n3 <=> x e n & 1 e n & c3 e n]
U Spec, 34
36 (x,1,s(x)) e n3 <=> x e n & 1 e n & s(x) e n
U Spec, 35
37 [(x,1,s(x)) e n3 => x e n & 1 e n & s(x) e n]
& [x e n & 1 e n & s(x) e n => (x,1,s(x)) e n3]
Iff-And, 36
38 (x,1,s(x)) e n3 => x e n & 1 e n & s(x) e n
Split, 37
39 x e n & 1 e n & s(x) e n => (x,1,s(x)) e n3
Split, 37
40 x e n => s(x) e n
U Spec, 3
41 s(x) e n
Detach, 40, 27
42 x e n & 1 e n
Join, 27, 2
43 x e n & 1 e n & s(x) e n
Join, 42, 41
As Required:
44 (x,1,s(x)) e n3
Detach, 39, 43
Prove: ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,s(x)) e d]
Suppose...
45 d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
Premise
46 d e pn3
Split, 45
47 ALL(e):[e e n => (e,1,s(e)) e d]
Split, 45
48 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
Split, 45
49 x e n => (x,1,s(x)) e d
U Spec, 47
50 (x,1,s(x)) e d
Detach, 49, 27
As Required:
51 ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,s(x)) e d]
4 Conclusion, 45
52 (x,1,s(x)) e n3
& ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,s(x)) e d]
Join, 44, 51
53 (x,1,s(x)) e add
Detach, 33, 52
As Required:
54 ALL(a):[a e n => (a,1,s(a)) e add]
4 Conclusion, 27
Prove: ALL(a):ALL(b):ALL(c):[(a,b,c) e add
=> (a,b,c) e n3 & [a e n & b e n & c e n]]
Suppose...
55 (x,y,z) e add
Premise
56 ALL(b):ALL(c):[(x,b,c) e add
<=> (x,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,b,c) e d]]
U Spec, 26
57 ALL(c):[(x,y,c) e add
<=> (x,y,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,c) e d]]
U Spec, 56
58 (x,y,z) e add
<=> (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,z) e d]
U Spec, 57
59 [(x,y,z) e add => (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,z) e d]]
& [(x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,z) e d] => (x,y,z) e add]
Iff-And, 58
60 (x,y,z) e add => (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,z) e d]
Split, 59
61 (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,z) e d] => (x,y,z) e add
Split, 59
62 (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,z) e d]
Detach, 60, 55
63 (x,y,z) e n3
Split, 62
64 ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,z) e d]
Split, 62
65 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 16
66 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 65
67 (x,y,z) e n3 <=> x e n & y e n & z e n
U Spec, 66
68 [(x,y,z) e n3 => x e n & y e n & z e n]
& [x e n & y e n & z e n => (x,y,z) e n3]
Iff-And, 67
69 (x,y,z) e n3 => x e n & y e n & z e n
Split, 68
70 x e n & y e n & z e n => (x,y,z) e n3
Split, 68
71 x e n & y e n & z e n
Detach, 69, 63
72 (x,y,z) e n3 & [x e n & y e n & z e n]
Join, 63, 71
As Required:
73 ALL(a):ALL(b):ALL(c):[(a,b,c) e add
=> (a,b,c) e n3 & [a e n & b e n & c e n]]
4 Conclusion, 55
Prove: ALL(a):ALL(b):ALL(c):[(a,b,c) e add => (a,s(b),s(c)) e add]
Suppose...
74 (x,y,z) e add
Premise
75 ALL(b):ALL(c):[(x,b,c) e add
=> (x,b,c) e n3 & [x e n & b e n & c e n]]
U Spec, 73
76 ALL(c):[(x,y,c) e add
=> (x,y,c) e n3 & [x e n & y e n & c e n]]
U Spec, 75
77 (x,y,z) e add
=> (x,y,z) e n3 & [x e n & y e n & z e n]
U Spec, 76
78 (x,y,z) e n3 & [x e n & y e n & z e n]
Detach, 77, 74
79 (x,y,z) e n3
Split, 78
80 x e n & y e n & z e n
Split, 78
81 ALL(b):ALL(c):[(x,b,c) e add
<=> (x,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,b,c) e d]]
U Spec, 26
82 ALL(c):[(x,s(y),c) e add
<=> (x,s(y),c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),c) e d]]
U Spec, 81
83 (x,s(y),s(z)) e add
<=> (x,s(y),s(z)) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),s(z)) e d]
U Spec, 82
84 [(x,s(y),s(z)) e add => (x,s(y),s(z)) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),s(z)) e d]]
& [(x,s(y),s(z)) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),s(z)) e d] => (x,s(y),s(z)) e add]
Iff-And, 83
85 (x,s(y),s(z)) e add => (x,s(y),s(z)) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),s(z)) e d]
Split, 84
86 x e n
Split, 80
87 y e n
Split, 80
88 z e n
Split, 80
Sufficient: For (x,s(y),s(z)) e add
89 (x,s(y),s(z)) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),s(z)) e d] => (x,s(y),s(z)) e add
Split, 84
90 ALL(b):ALL(c):[(x,b,c) e add
<=> (x,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,b,c) e d]]
U Spec, 26
91 ALL(c):[(x,y,c) e add
<=> (x,y,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,c) e d]]
U Spec, 90
92 (x,y,z) e add
<=> (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,z) e d]
U Spec, 91
93 [(x,y,z) e add => (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,z) e d]]
& [(x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,z) e d] => (x,y,z) e add]
Iff-And, 92
94 (x,y,z) e add => (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,z) e d]
Split, 93
95 (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,z) e d] => (x,y,z) e add
Split, 93
96 (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,z) e d]
Detach, 94, 74
97 (x,y,z) e n3
Split, 96
98 ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,z) e d]
Split, 96
99 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 16
100 ALL(c3):[(x,s(y),c3) e n3 <=> x e n & s(y) e n & c3 e n]
U Spec, 99
101 (x,s(y),s(z)) e n3 <=> x e n & s(y) e n & s(z) e n
U Spec, 100
102 [(x,s(y),s(z)) e n3 => x e n & s(y) e n & s(z) e n]
& [x e n & s(y) e n & s(z) e n => (x,s(y),s(z)) e n3]
Iff-And, 101
103 (x,s(y),s(z)) e n3 => x e n & s(y) e n & s(z) e n
Split, 102
104 x e n & s(y) e n & s(z) e n => (x,s(y),s(z)) e n3
Split, 102
105 y e n => s(y) e n
U Spec, 3
106 s(y) e n
Detach, 105, 87
107 z e n => s(z) e n
U Spec, 3
108 s(z) e n
Detach, 107, 88
109 x e n & s(y) e n
Join, 86, 106
110 x e n & s(y) e n & s(z) e n
Join, 109, 108
As Required:
111 (x,s(y),s(z)) e n3
Detach, 104, 110
Prove: ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),s(z)) e d]
Suppose...
112 d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
Premise
113 d e pn3
Split, 112
114 ALL(e):[e e n => (e,1,s(e)) e d]
Split, 112
115 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
Split, 112
116 ALL(f):ALL(g):[(x,f,g) e d => (x,s(f),s(g)) e d]
U Spec, 115
117 ALL(g):[(x,y,g) e d => (x,s(y),s(g)) e d]
U Spec, 116
118 (x,y,z) e d => (x,s(y),s(z)) e d
U Spec, 117
119 d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,y,z) e d
U Spec, 98
120 (x,y,z) e d
Detach, 119, 112
121 (x,s(y),s(z)) e d
Detach, 118, 120
As Required:
122 ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),s(z)) e d]
4 Conclusion, 112
123 (x,s(y),s(z)) e n3
& ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),s(z)) e d]
Join, 111, 122
124 (x,s(y),s(z)) e add
Detach, 89, 123
As Required:
125 ALL(a):ALL(b):ALL(c):[(a,b,c) e add => (a,s(b),s(c)) e add]
4 Conclusion, 74
Prove: ALL(a):[a e n => ALL(b):[(a,1,b) e add => [b e n => b=s(a)]]]
Suppose...
126 x e n
Premise
Prove: ALL(b):[b e n & ~b=s(x) => ~(x,1,b) e add]
Suppose...
127 y e n & ~y=s(x)
Premise
128 y e n
Split, 127
129 ~y=s(x)
Split, 127
130 ALL(b):ALL(c):[(x,b,c) e add
<=> (x,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,b,c) e d]]
U Spec, 26
131 ALL(c):[(x,1,c) e add
<=> (x,1,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,c) e d]]
U Spec, 130
132 (x,1,y) e add
<=> (x,1,y) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,y) e d]
U Spec, 131
133 [(x,1,y) e add => (x,1,y) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,y) e d]]
& [(x,1,y) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,y) e d] => (x,1,y) e add]
Iff-And, 132
134 (x,1,y) e add => (x,1,y) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,y) e d]
Split, 133
135 (x,1,y) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,y) e d] => (x,1,y) e add
Split, 133
136 ~[(x,1,y) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,y) e d]] => ~(x,1,y) e add
Contra, 134
137 ~~[~(x,1,y) e n3 | ~ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,y) e d]] => ~(x,1,y) e add
DeMorgan, 136
138 ~(x,1,y) e n3 | ~ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,y) e d] => ~(x,1,y) e add
Rem DNeg, 137
139 ~(x,1,y) e n3 | ~~EXIST(d):~[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,y) e d] => ~(x,1,y) e add
Quant, 138
140 ~(x,1,y) e n3 | EXIST(d):~[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,1,y) e d] => ~(x,1,y) e add
Rem DNeg, 139
141 ~(x,1,y) e n3 | EXIST(d):~~[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g)
e d => (e,s(f),s(g))
e d] & ~(x,1,y)
e d]
=> ~(x,1,y)
e add
Imply-And, 140
Sufficient: For ~(x,1,y) e add
142 ~(x,1,y) e n3 | EXIST(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g)
e d => (e,s(f),s(g))
e d] & ~(x,1,y)
e d]
=> ~(x,1,y)
e add
Rem DNeg, 141
143 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=> (a,b,c) e add & ~[a=x & b=1 & c=y]]]
Subset, 25
144 Set''(p) & ALL(a):ALL(b):ALL(c):[(a,b,c) e p
<=> (a,b,c) e add & ~[a=x & b=1 & c=y]]
E Spec, 143
Define: p
*********
145 Set''(p)
Split, 144
146 ALL(a):ALL(b):ALL(c):[(a,b,c) e p
<=> (a,b,c) e add & ~[a=x & b=1 & c=y]]
Split, 144
147 p e pn3 <=> Set''(p) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e p => (d1,d2,d3) e n3]
U Spec, 22
148 [p e pn3 => Set''(p) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e p => (d1,d2,d3) e n3]]
& [Set''(p) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e p => (d1,d2,d3) e n3] => p e pn3]
Iff-And, 147
149 p e pn3 => Set''(p) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e p => (d1,d2,d3) e n3]
Split, 148
Sufficient: For p e pn3
150 Set''(p) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e p => (d1,d2,d3) e n3] => p e pn3
Split, 148
Prove: ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e p => (d1,d2,d3) e n3]
Suppose...
151 (t,u,v) e p
Premise
152 ALL(b):ALL(c):[(t,b,c) e p
<=> (t,b,c) e add & ~[t=x & b=1 & c=y]]
U Spec, 146
153 ALL(c):[(t,u,c) e p
<=> (t,u,c) e add & ~[t=x & u=1 & c=y]]
U Spec, 152
154 (t,u,v) e p
<=> (t,u,v) e add & ~[t=x & u=1 & v=y]
U Spec, 153
155 [(t,u,v) e p => (t,u,v) e add & ~[t=x & u=1 & v=y]]
& [(t,u,v) e add & ~[t=x & u=1 & v=y] => (t,u,v) e p]
Iff-And, 154
156 (t,u,v) e p => (t,u,v) e add & ~[t=x & u=1 & v=y]
Split, 155
157 (t,u,v) e add & ~[t=x & u=1 & v=y] => (t,u,v) e p
Split, 155
158 (t,u,v) e add & ~[t=x & u=1 & v=y]
Detach, 156, 151
159 (t,u,v) e add
Split, 158
160 ~[t=x & u=1 & v=y]
Split, 158
161 ALL(b):ALL(c):[(t,b,c) e add
=> (t,b,c) e n3 & [t e n & b e n & c e n]]
U Spec, 73
162 ALL(c):[(t,u,c) e add
=> (t,u,c) e n3 & [t e n & u e n & c e n]]
U Spec, 161
163 (t,u,v) e add
=> (t,u,v) e n3 & [t e n & u e n & v e n]
U Spec, 162
164 (t,u,v) e n3 & [t e n & u e n & v e n]
Detach, 163, 159
165 (t,u,v) e n3
Split, 164
As Required:
166 ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e p => (d1,d2,d3) e n3]
4 Conclusion, 151
167 Set''(p)
& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e p => (d1,d2,d3) e n3]
Join, 145, 166
As Required:
168 p e pn3
Detach, 150, 167
Prove: ALL(e):[e e n => (e,1,s(e)) e p]
Suppose...
169 t e n
Premise
170 ALL(b):ALL(c):[(t,b,c) e p
<=> (t,b,c) e add & ~[t=x & b=1 & c=y]]
U Spec, 146
171 ALL(c):[(t,1,c) e p
<=> (t,1,c) e add & ~[t=x & 1=1 & c=y]]
U Spec, 170
172 (t,1,s(t)) e p
<=> (t,1,s(t)) e add & ~[t=x & 1=1 & s(t)=y]
U Spec, 171
173 [(t,1,s(t)) e p => (t,1,s(t)) e add & ~[t=x & 1=1 & s(t)=y]]
& [(t,1,s(t)) e add & ~[t=x & 1=1 & s(t)=y] => (t,1,s(t)) e p]
Iff-And, 172
174 (t,1,s(t)) e p => (t,1,s(t)) e add & ~[t=x & 1=1 & s(t)=y]
Split, 173
Sufficient: For (t,1,s(t)) e p
175 (t,1,s(t)) e add & ~[t=x & 1=1 & s(t)=y] => (t,1,s(t)) e p
Split, 173
176 t e n => (t,1,s(t)) e add
U Spec, 54
As Required:
177 (t,1,s(t)) e add
Detach, 176, 169
Prove: ~[t=x & 1=1 & s(t)=y]
Suppose to the contrary...
178 t=x & 1=1 & s(t)=y
Premise
179 t=x
Split, 178
180 1=1
Split, 178
181 s(t)=y
Split, 178
182 s(x)=y
Substitute, 179, 181
183 y=s(x)
Sym, 182
184 y=s(x) & ~y=s(x)
Join, 183, 129
As Required:
185 ~[t=x & 1=1 & s(t)=y]
4 Conclusion, 178
186 (t,1,s(t)) e add & ~[t=x & 1=1 & s(t)=y]
Join, 177, 185
187 (t,1,s(t)) e p
Detach, 175, 186
As Required:
188 ALL(e):[e e n => (e,1,s(e)) e p]
4 Conclusion, 169
Prove: ALL(e):ALL(f):ALL(g):[(e,f,g) e p => (e,s(f),s(g)) e p]
Suppose...
189 (t,u,v) e p
Premise
190 ALL(b):ALL(c):[(t,b,c) e p
<=> (t,b,c) e add & ~[t=x & b=1 & c=y]]
U Spec, 146
191 ALL(c):[(t,u,c) e p
<=> (t,u,c) e add & ~[t=x & u=1 & c=y]]
U Spec, 190
192 (t,u,v) e p
<=> (t,u,v) e add & ~[t=x & u=1 & v=y]
U Spec, 191
193 [(t,u,v) e p => (t,u,v) e add & ~[t=x & u=1 & v=y]]
& [(t,u,v) e add & ~[t=x & u=1 & v=y] => (t,u,v) e p]
Iff-And, 192
194 (t,u,v) e p => (t,u,v) e add & ~[t=x & u=1 & v=y]
Split, 193
195 (t,u,v) e add & ~[t=x & u=1 & v=y] => (t,u,v) e p
Split, 193
196 (t,u,v) e add & ~[t=x & u=1 & v=y]
Detach, 194, 189
197 (t,u,v) e add
Split, 196
198 ~[t=x & u=1 & v=y]
Split, 196
199 ALL(b):ALL(c):[(t,b,c) e add => (t,s(b),s(c)) e add]
U Spec, 125
200 ALL(c):[(t,u,c) e add => (t,s(u),s(c)) e add]
U Spec, 199
201 (t,u,v) e add => (t,s(u),s(v)) e add
U Spec, 200
As Required:
202 (t,s(u),s(v)) e add
Detach, 201, 197
203 ALL(b):ALL(c):[(t,b,c) e p
<=> (t,b,c) e add & ~[t=x & b=1 & c=y]]
U Spec, 146
204 ALL(c):[(t,s(u),c) e p
<=> (t,s(u),c) e add & ~[t=x & s(u)=1 & c=y]]
U Spec, 203
205 (t,s(u),s(v)) e p
<=> (t,s(u),s(v)) e add & ~[t=x & s(u)=1 & s(v)=y]
U Spec, 204
206 [(t,s(u),s(v)) e p => (t,s(u),s(v)) e add & ~[t=x & s(u)=1 & s(v)=y]]
& [(t,s(u),s(v)) e add & ~[t=x & s(u)=1 & s(v)=y] => (t,s(u),s(v)) e p]
Iff-And, 205
207 (t,s(u),s(v)) e p => (t,s(u),s(v)) e add & ~[t=x & s(u)=1 & s(v)=y]
Split, 206
Sufficient: For (t,s(u),s(v)) e p
208 (t,s(u),s(v)) e add & ~[t=x & s(u)=1 & s(v)=y] => (t,s(u),s(v)) e p
Split, 206
Prove: ~[t=x & s(u)=1 & s(v)=y]
Suppose to the contrary...
209 t=x & s(u)=1 & s(v)=y
Premise
210 t=x
Split, 209
211 s(u)=1
Split, 209
212 s(v)=y
Split, 209
213 u e n => ~s(u)=1
U Spec, 5
214 ALL(b):ALL(c):[(t,b,c) e add
=> (t,b,c) e n3 & [t e n & b e n & c e n]]
U Spec, 73
215 ALL(c):[(t,u,c) e add
=> (t,u,c) e n3 & [t e n & u e n & c e n]]
U Spec, 214
216 (t,u,v) e add
=> (t,u,v) e n3 & [t e n & u e n & v e n]
U Spec, 215
217 (t,u,v) e n3 & [t e n & u e n & v e n]
Detach, 216, 197
218 (t,u,v) e n3
Split, 217
219 t e n & u e n & v e n
Split, 217
220 t e n
Split, 219
221 u e n
Split, 219
222 v e n
Split, 219
223 ~s(u)=1
Detach, 213, 221
224 s(u)=1 & ~s(u)=1
Join, 211, 223
As Required:
225 ~[t=x & s(u)=1 & s(v)=y]
4 Conclusion, 209
226 (t,s(u),s(v)) e add & ~[t=x & s(u)=1 & s(v)=y]
Join, 202, 225
227 (t,s(u),s(v)) e p
Detach, 208, 226
As Required:
228 ALL(e):ALL(f):ALL(g):[(e,f,g) e p => (e,s(f),s(g)) e p]
4 Conclusion, 189
229 ALL(b):ALL(c):[(x,b,c) e p
<=> (x,b,c) e add & ~[x=x & b=1 & c=y]]
U Spec, 146
230 ALL(c):[(x,1,c) e p
<=> (x,1,c) e add & ~[x=x & 1=1 & c=y]]
U Spec, 229
231 (x,1,y) e p
<=> (x,1,y) e add & ~[x=x & 1=1 & y=y]
U Spec, 230
232 [(x,1,y) e p => (x,1,y) e add & ~[x=x & 1=1 & y=y]]
& [(x,1,y) e add & ~[x=x & 1=1 & y=y] => (x,1,y) e p]
Iff-And, 231
233 (x,1,y) e p => (x,1,y) e add & ~[x=x & 1=1 & y=y]
Split, 232
234 (x,1,y) e add & ~[x=x & 1=1 & y=y] => (x,1,y) e p
Split, 232
235 ~[(x,1,y) e add & ~[x=x & 1=1 & y=y]] => ~(x,1,y) e p
Contra, 233
236 ~~[~(x,1,y) e add | ~~[x=x & 1=1 & y=y]] => ~(x,1,y) e p
DeMorgan, 235
237 ~(x,1,y) e add | ~~[x=x & 1=1 & y=y] => ~(x,1,y) e p
Rem DNeg, 236
Sufficient: For ~(x,1,y) e p
238 ~(x,1,y) e add | x=x & 1=1 & y=y => ~(x,1,y) e p
Rem DNeg, 237
239 x=x
Reflex
240 1=1
Reflex
241 y=y
Reflex
242 x=x & 1=1
Join, 239, 240
243 x=x & 1=1 & y=y
Join, 242, 241
244 ~(x,1,y) e add | x=x & 1=1 & y=y
Arb Or, 243
As Required:
245 ~(x,1,y) e p
Detach, 238, 244
246 p e pn3 & ALL(e):[e e n => (e,1,s(e)) e p]
Join, 168, 188
247 p e pn3 & ALL(e):[e e n => (e,1,s(e)) e p]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e p => (e,s(f),s(g)) e p]
Join, 246, 228
248 p e pn3 & ALL(e):[e e n => (e,1,s(e)) e p]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e p => (e,s(f),s(g)) e p]
& ~(x,1,y) e p
Join, 247, 245
249 EXIST(d):[d e pn3 & ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
& ~(x,1,y) e d]
E Gen, 248
250 ~(x,1,y) e n3 | EXIST(d):[d e pn3 & ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
& ~(x,1,y) e d]
Arb Or, 249
251 ~(x,1,y) e add
Detach, 142, 250
As Required:
252 ALL(b):[b e n & ~b=s(x) => ~(x,1,b) e add]
4 Conclusion, 127
253 ALL(b):[~~(x,1,b) e add => ~[b e n & ~b=s(x)]]
Contra, 252
254 ALL(b):[(x,1,b) e add => ~[b e n & ~b=s(x)]]
Rem DNeg, 253
255 ALL(b):[(x,1,b) e add => ~~[b e n => ~~b=s(x)]]
Imply-And, 254
256 ALL(b):[(x,1,b) e add => [b e n => ~~b=s(x)]]
Rem DNeg, 255
257 ALL(b):[(x,1,b) e add => [b e n => b=s(x)]]
Rem DNeg, 256
As Required:
258 ALL(a):[a e n => ALL(b):[(a,1,b) e add => [b e n => b=s(a)]]]
4 Conclusion, 126
Prove: ALL(a):ALL(b):[a e n & b e n => [(a,1,b) e add => b=s(a)]]
Suppose...
259 x e n & y e n
Premise
260 x e n
Split, 259
261 y e n
Split, 259
262 x e n => ALL(b):[(x,1,b) e add => [b e n => b=s(x)]]
U Spec, 258
263 ALL(b):[(x,1,b) e add => [b e n => b=s(x)]]
Detach, 262, 260
264 (x,1,y) e add => [y e n => y=s(x)]
U Spec, 263
Prove: (x,1,y) e add => y=s(x)
Suppose...
265 (x,1,y) e add
Premise
266 y e n => y=s(x)
Detach, 264, 265
267 y=s(x)
Detach, 266, 261
As Required:
268 (x,1,y) e add => y=s(x)
4 Conclusion, 265
As Required:
269 ALL(a):ALL(b):[a e n & b e n => [(a,1,b) e add => b=s(a)]]
4 Conclusion, 259
Apply Function axiom
270 ALL(f):ALL(a1):ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e f => c1 e a1 & c2 e a2 & d e b]
& ALL(c1):ALL(c2):[c1 e a1 & c2 e a2 => EXIST(d):[d e b & (c1,c2,d) e f]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e f & (c1,c2,d2) e f => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=f(c1,c2) <=> (c1,c2,d) e f]]
Function
271 ALL(a1):ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => c1 e a1 & c2 e a2 & d e b]
& ALL(c1):ALL(c2):[c1 e a1 & c2 e a2 => EXIST(d):[d e b & (c1,c2,d) e add]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) e add]]
U Spec, 270
272 ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => c1 e n & c2 e a2 & d e b]
& ALL(c1):ALL(c2):[c1 e n & c2 e a2 => EXIST(d):[d e b & (c1,c2,d) e add]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) e add]]
U Spec, 271
273 ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => c1 e n & c2 e n & d e b]
& ALL(c1):ALL(c2):[c1 e n & c2 e n => EXIST(d):[d e b & (c1,c2,d) e add]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) e add]]
U Spec, 272
Sufficient: For functionality of add
274 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => c1 e n & c2 e n & d e n]
& ALL(c1):ALL(c2):[c1 e n & c2 e n => EXIST(d):[d e n & (c1,c2,d) e add]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) e add]
U Spec, 273
Prove: ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => c1 e n & c2 e n & d e n]
Suppose...
275 (x,y,z) e add
Premise
276 ALL(b):ALL(c):[(x,b,c) e add
=> (x,b,c) e n3 & [x e n & b e n & c e n]]
U Spec, 73
277 ALL(c):[(x,y,c) e add
=> (x,y,c) e n3 & [x e n & y e n & c e n]]
U Spec, 276
278 (x,y,z) e add
=> (x,y,z) e n3 & [x e n & y e n & z e n]
U Spec, 277
279 (x,y,z) e n3 & [x e n & y e n & z e n]
Detach, 278, 275
280 (x,y,z) e n3
Split, 279
281 x e n & y e n & z e n
Split, 279
Functionality of add: Part 1
As Required:
282 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => c1 e n & c2 e n & d e n]
4 Conclusion, 275
Prove: ALL(c):[c e n
=> ALL(a):[a e n => EXIST(b):[b e n & (c,a,b) e add]]]
Suppose...
283 x e n
Premise
Prove by induction that for elements a e n, there exists b e n such that (x,a,b) e add.
Apply the Subset axiom to construct the set of all such numbers.
284 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & EXIST(b):[b e n & (x,a,b) e add]]]
Subset, 1
285 Set(q) & ALL(a):[a e q <=> a e n & EXIST(b):[b e n & (x,a,b) e add]]
E Spec, 284
Define: q
*********
286 Set(q)
Split, 285
287 ALL(a):[a e q <=> a e n & EXIST(b):[b e n & (x,a,b) e add]]
Split, 285
Apply the Principle of Mathematical Induction from Peano's Axioms
288 Set(q) & ALL(b):[b e q => b e n]
=> [1 e q & ALL(b):[b e q => s(b) e q]
=> ALL(b):[b e n => b e q]]
U Spec, 6
Prove: ALL(b):[b e q => b e n]
Suppose...
289 y e q
Premise
290 y e q <=> y e n & EXIST(b):[b e n & (x,y,b) e add]
U Spec, 287
291 [y e q => y e n & EXIST(b):[b e n & (x,y,b) e add]]
& [y e n & EXIST(b):[b e n & (x,y,b) e add] => y e q]
Iff-And, 290
292 y e q => y e n & EXIST(b):[b e n & (x,y,b) e add]
Split, 291
293 y e n & EXIST(b):[b e n & (x,y,b) e add] => y e q
Split, 291
294 y e n & EXIST(b):[b e n & (x,y,b) e add]
Detach, 292, 289
295 y e n
Split, 294
As Required:
296 ALL(b):[b e q => b e n]
4 Conclusion, 289
297 Set(q) & ALL(b):[b e q => b e n]
Join, 286, 296
Sufficient: ALL(b):[b e n => b e q]
298 1 e q & ALL(b):[b e q => s(b) e q]
=> ALL(b):[b e n => b e q]
Detach, 288, 297
Base Case
Prove: 1 e q
Apply definition of q
299 1 e q <=> 1 e n & EXIST(b):[b e n & (x,1,b) e add]
U Spec, 287
300 [1 e q => 1 e n & EXIST(b):[b e n & (x,1,b) e add]]
& [1 e n & EXIST(b):[b e n & (x,1,b) e add] => 1 e q]
Iff-And, 299
301 1 e q => 1 e n & EXIST(b):[b e n & (x,1,b) e add]
Split, 300
Sufficient: For 1 e q
302 1 e n & EXIST(b):[b e n & (x,1,b) e add] => 1 e q
Split, 300
303 x e n => (x,1,s(x)) e add
U Spec, 54
304 (x,1,s(x)) e add
Detach, 303, 283
305 x e n => s(x) e n
U Spec, 3
306 s(x) e n
Detach, 305, 283
307 s(x) e n & (x,1,s(x)) e add
Join, 306, 304
308 EXIST(b):[b e n & (x,1,b) e add]
E Gen, 307
309 1 e n & EXIST(b):[b e n & (x,1,b) e add]
Join, 2, 308
As Required:
310 1 e q
Detach, 302, 309
Inductive Step
Prove: ALL(b):[b e q => s(b) e q
Suppose...
311 y e q
Premise
312 y e q <=> y e n & EXIST(b):[b e n & (x,y,b) e add]
U Spec, 287
313 [y e q => y e n & EXIST(b):[b e n & (x,y,b) e add]]
& [y e n & EXIST(b):[b e n & (x,y,b) e add] => y e q]
Iff-And, 312
314 y e q => y e n & EXIST(b):[b e n & (x,y,b) e add]
Split, 313
315 y e n & EXIST(b):[b e n & (x,y,b) e add] => y e q
Split, 313
316 y e n & EXIST(b):[b e n & (x,y,b) e add]
Detach, 314, 311
317 y e n
Split, 316
318 EXIST(b):[b e n & (x,y,b) e add]
Split, 316
319 z e n & (x,y,z) e add
E Spec, 318
320 z e n
Split, 319
321 (x,y,z) e add
Split, 319
322 s(y) e q <=> s(y) e n & EXIST(b):[b e n & (x,s(y),b) e add]
U Spec, 287
323 [s(y) e q => s(y) e n & EXIST(b):[b e n & (x,s(y),b) e add]]
& [s(y) e n & EXIST(b):[b e n & (x,s(y),b) e add] => s(y) e q]
Iff-And, 322
324 s(y) e q => s(y) e n & EXIST(b):[b e n & (x,s(y),b) e add]
Split, 323
Sufficient: For s(y) e q
325 s(y) e n & EXIST(b):[b e n & (x,s(y),b) e add] => s(y) e q
Split, 323
326 y e n => s(y) e n
U Spec, 3
327 y e q => y e n
U Spec, 296
328 y e n
Detach, 327, 311
329 s(y) e n
Detach, 326, 328
330 ALL(b):ALL(c):[(x,b,c) e add => (x,s(b),s(c)) e add]
U Spec, 125
331 ALL(c):[(x,y,c) e add => (x,s(y),s(c)) e add]
U Spec, 330
332 (x,y,z) e add => (x,s(y),s(z)) e add
U Spec, 331
333 (x,s(y),s(z)) e add
Detach, 332, 321
334 z e n => s(z) e n
U Spec, 3
335 s(z) e n
Detach, 334, 320
336 s(z) e n & (x,s(y),s(z)) e add
Join, 335, 333
337 EXIST(b):[b e n & (x,s(y),b) e add]
E Gen, 336
338 s(y) e n & EXIST(b):[b e n & (x,s(y),b) e add]
Join, 329, 337
339 s(y) e q
Detach, 325, 338
As Required:
340 ALL(b):[b e q => s(b) e q]
4 Conclusion, 311
341 1 e q & ALL(b):[b e q => s(b) e q]
Join, 310, 340
342 ALL(b):[b e n => b e q]
Detach, 298, 341
Prove: ALL(a):[a e n => EXIST(b):[b e n & (x,a,b) e add]]
Suppose...
343 y e n
Premise
344 y e n => y e q
U Spec, 342
345 y e q
Detach, 344, 343
346 y e q <=> y e n & EXIST(b):[b e n & (x,y,b) e add]
U Spec, 287
347 [y e q => y e n & EXIST(b):[b e n & (x,y,b) e add]]
& [y e n & EXIST(b):[b e n & (x,y,b) e add] => y e q]
Iff-And, 346
348 y e q => y e n & EXIST(b):[b e n & (x,y,b) e add]
Split, 347
349 y e n & EXIST(b):[b e n & (x,y,b) e add] => y e q
Split, 347
350 y e n & EXIST(b):[b e n & (x,y,b) e add]
Detach, 348, 345
351 y e n
Split, 350
352 EXIST(b):[b e n & (x,y,b) e add]
Split, 350
As Required:
353 ALL(a):[a e n => EXIST(b):[b e n & (x,a,b) e add]]
4 Conclusion, 343
As Required:
354 ALL(c):[c e n
=> ALL(a):[a e n => EXIST(b):[b e n & (c,a,b) e add]]]
4 Conclusion, 283
Prove: ALL(c1):ALL(c2):[c1 e n & c2 e n => EXIST(b):[b e n & (c1,c2,b) e add]]
Suppose...
355 x e n & y e n
Premise
356 x e n
Split, 355
357 y e n
Split, 355
358 x e n
=> ALL(a):[a e n => EXIST(b):[b e n & (x,a,b) e add]]
U Spec, 354
359 ALL(a):[a e n => EXIST(b):[b e n & (x,a,b) e add]]
Detach, 358, 356
360 y e n => EXIST(b):[b e n & (x,y,b) e add]
U Spec, 359
361 EXIST(b):[b e n & (x,y,b) e add]
Detach, 360, 357
Functionality of add: Part 2
As Required:
362 ALL(c1):ALL(c2):[c1 e n & c2 e n => EXIST(b):[b e n & (c1,c2,b) e add]]
4 Conclusion, 355
Prove: ALL(a):[a e n
=> ALL(b):[b e n
=> ALL(c1):ALL(c2):[(a,b,c1) e add & (a,b,c2) e add => c1=c2]]]
Suppose...
363 x e n
Premise
Prove by induction
that for all elements b
e
n, if (x,b,c1) e
add and (x,b,c2) e
add
then c1 = c2.
Apply Subset axiom to construct the set of all such numbers.
364
EXIST(sub):[Set(sub)
& ALL(b):[b e
sub <=> b
e n
& ALL(c1):ALL(c2):[(x,b,c1)
e add
& (x,b,c2)
e add
=> c1=c2]]]
Subset, 1
365
Set(r)
& ALL(b):[b e
r
<=> b e
n
& ALL(c1):ALL(c2):[(x,b,c1)
e add
& (x,b,c2)
e add
=> c1=c2]]
E Spec, 364
Define: r
366 Set(r)
Split, 365
367 ALL(b):[b e r <=> b e n & ALL(c1):ALL(c2):[(x,b,c1) e add & (x,b,c2) e add => c1=c2]]
Split, 365
368 Set(r) & ALL(b):[b e r => b e n]
=> [1 e r & ALL(b):[b e r => s(b) e r]
=> ALL(b):[b e n => b e r]]
U Spec, 6
Prove: ALL(b):[b e r => b e n]
Suppose...
369 y e r
Premise
370 y e r <=> y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2]
U Spec, 367
371 [y e r => y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2]]
& [y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2] => y e r]
Iff-And, 370
372 y e r => y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2]
Split, 371
373 y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2] => y e r
Split, 371
374 y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2]
Detach, 372, 369
375 y e n
Split, 374
As Required:
376 ALL(b):[b e r => b e n]
4 Conclusion, 369
377 Set(r) & ALL(b):[b e r => b e n]
Join, 366, 376
Sufficient: For ALL(b):[b e n => b e r]
378 1 e r & ALL(b):[b e r => s(b) e r]
=> ALL(b):[b e n => b e r]
Detach, 368, 377
Base Case
Prove: 1 e r
Apply definition of r
379 1 e r <=> 1 e n & ALL(c1):ALL(c2):[(x,1,c1) e add & (x,1,c2) e add => c1=c2]
U Spec, 367
380 [1 e r => 1 e n & ALL(c1):ALL(c2):[(x,1,c1) e add & (x,1,c2) e add => c1=c2]]
& [1 e n & ALL(c1):ALL(c2):[(x,1,c1) e add & (x,1,c2) e add => c1=c2] => 1 e r]
Iff-And, 379
381 1 e r => 1 e n & ALL(c1):ALL(c2):[(x,1,c1) e add & (x,1,c2) e add => c1=c2]
Split, 380
Sufficient: For 1 e r
382 1 e n & ALL(c1):ALL(c2):[(x,1,c1) e add & (x,1,c2) e add => c1=c2] => 1 e r
Split, 380
Prove: ALL(c1):ALL(c2):[(x,1,c1) e add & (x,1,c2) e add => c1=c2]
Suppose...
383 (x,1,z1) e add & (x,1,z2) e add
Premise
384 (x,1,z1) e add
Split, 383
385 (x,1,z2) e add
Split, 383
386 ALL(b):[x e n & b e n => [(x,1,b) e add => b=s(x)]]
U Spec, 269
387 x e n & z1 e n => [(x,1,z1) e add => z1=s(x)]
U Spec, 386
388 ALL(b):ALL(c):[(x,b,c) e add
=> (x,b,c) e n3 & [x e n & b e n & c e n]]
U Spec, 73
389 ALL(c):[(x,1,c) e add
=> (x,1,c) e n3 & [x e n & 1 e n & c e n]]
U Spec, 388
390 (x,1,z1) e add
=> (x,1,z1) e n3 & [x e n & 1 e n & z1 e n]
U Spec, 389
391 (x,1,z1) e n3 & [x e n & 1 e n & z1 e n]
Detach, 390, 384
392 (x,1,z1) e n3
Split, 391
393 x e n & 1 e n & z1 e n
Split, 391
394 x e n
Split, 393
395 1 e n
Split, 393
396 z1 e n
Split, 393
397 x e n & z1 e n
Join, 363, 396
398 (x,1,z1) e add => z1=s(x)
Detach, 387, 397
399 z1=s(x)
Detach, 398, 384
400 x e n & z2 e n => [(x,1,z2) e add => z2=s(x)]
U Spec, 386
401 (x,1,z2) e add
=> (x,1,z2) e n3 & [x e n & 1 e n & z2 e n]
U Spec, 389
402 (x,1,z2) e n3 & [x e n & 1 e n & z2 e n]
Detach, 401, 385
403 (x,1,z2) e n3
Split, 402
404 x e n & 1 e n & z2 e n
Split, 402
405 x e n
Split, 404
406 1 e n
Split, 404
407 z2 e n
Split, 404
408 x e n & z2 e n
Join, 363, 407
409 (x,1,z2) e add => z2=s(x)
Detach, 400, 408
410 z2=s(x)
Detach, 409, 385
411 z1=z2
Substitute, 410, 399
As Required:
412 ALL(c1):ALL(c2):[(x,1,c1) e add & (x,1,c2) e add => c1=c2]
4 Conclusion, 383
413 1 e n
& ALL(c1):ALL(c2):[(x,1,c1) e add & (x,1,c2) e add => c1=c2]
Join, 2, 412
As Required:
414 1 e r
Detach, 382, 413
Inductive Step
Prove: ALL(b):[b e r => s(b) e r]
Suppose...
415 y e r
Premise
416 y e r <=> y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2]
U Spec, 367
417 [y e r => y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2]]
& [y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2] => y e r]
Iff-And, 416
418 y e r => y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2]
Split, 417
419 y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2] => y e r
Split, 417
420 y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2]
Detach, 418, 415
421 y e n
Split, 420
Sum of x and y is unique
422 ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2]
Split, 420
423
s(y)
e r
<=> s(y)
e n
& ALL(c1):ALL(c2):[(x,s(y),c1)
e add
& (x,s(y),c2)
e add
=> c1=c2]
U Spec, 367
424
[s(y)
e r
=> s(y)
e n
& ALL(c1):ALL(c2):[(x,s(y),c1)
e add
& (x,s(y),c2)
e add
=> c1=c2]]
& [s(y)
e n
& ALL(c1):ALL(c2):[(x,s(y),c1)
e add
& (x,s(y),c2)
e add
=> c1=c2]
=> s(y)
e r]
Iff-And, 423
425 s(y) e r => s(y) e n & ALL(c1):ALL(c2):[(x,s(y),c1) e add & (x,s(y),c2) e add => c1=c2]
Split, 424
Sufficient: For s(y) e r
426 s(y) e n & ALL(c1):ALL(c2):[(x,s(y),c1) e add & (x,s(y),c2) e add => c1=c2] => s(y) e r
Split, 424
427 y e n => s(y) e n
U Spec, 3
As Required:
428 s(y) e n
Detach, 427, 421
429 ALL(c2):[x e n & c2 e n => EXIST(b):[b e n & (x,c2,b) e add]]
U Spec, 362
430 x e n & y e n => EXIST(b):[b e n & (x,y,b) e add]
U Spec, 429
431 x e n & y e n
Join, 363, 421
432 EXIST(b):[b e n & (x,y,b) e add]
Detach, 430, 431
433 z e n & (x,y,z) e add
E Spec, 432
Define: z
434 z e n
Split, 433
435 (x,y,z) e add
Split, 433
Prove: ALL(c):[c e n => [(x,y,c) e add => z=c]]
Suppose...
436 z' e n
Premise
437 ALL(c2):[(x,y,z) e add & (x,y,c2) e add => z=c2]
U Spec, 422
438 (x,y,z) e add & (x,y,z') e add => z=z'
U Spec, 437
Prove: (x,y,z') e add => z=z'
Suppose...
439 (x,y,z') e add
Premise
440 (x,y,z) e add & (x,y,z') e add
Join, 435, 439
441 z=z'
Detach, 438, 440
As Required:
442 (x,y,z') e add => z=z'
4 Conclusion, 439
As Required:
443 ALL(c):[c e n => [(x,y,c) e add => z=c]]
4 Conclusion, 436
Prove: ALL(c):[c e n => [(x,s(y),c) e add => c=s(z)]]
Suppose...
444 z' e n
Premise
Prove: ~[(x,s(y),z') e add & ~z'=s(z)]
Suppose to the contrary...
445 (x,s(y),z') e add & ~z'=s(z)
Premise
446 (x,s(y),z') e add
Split, 445
447 ~z'=s(z)
Split, 445
448 (x,s(y),z') e add
Split, 445
449 ~z'=s(z)
Split, 445
450 ALL(b):ALL(c):[(x,b,c) e add
<=> (x,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,b,c) e d]]
U Spec, 26
451 ALL(c):[(x,s(y),c) e add
<=> (x,s(y),c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),c) e d]]
U Spec, 450
452 (x,s(y),z') e add
<=> (x,s(y),z') e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),z') e d]
U Spec, 451
453 [(x,s(y),z') e add => (x,s(y),z') e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),z') e d]]
& [(x,s(y),z') e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),z') e d] => (x,s(y),z') e add]
Iff-And, 452
454 (x,s(y),z') e add => (x,s(y),z') e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),z') e d]
Split, 453
455 (x,s(y),z') e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),z') e d] => (x,s(y),z') e add
Split, 453
456 ~[(x,s(y),z') e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),z') e d]] => ~(x,s(y),z') e add
Contra, 454
457 ~~[~(x,s(y),z') e n3 | ~ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),z') e d]] => ~(x,s(y),z') e add
DeMorgan, 456
458 ~(x,s(y),z') e n3 | ~ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),z') e d] => ~(x,s(y),z') e add
Rem DNeg, 457
459 ~(x,s(y),z') e n3 | ~~EXIST(d):~[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),z') e d] => ~(x,s(y),z') e add
Quant, 458
460 ~(x,s(y),z') e n3 | EXIST(d):~[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=> (x,s(y),z') e d] => ~(x,s(y),z') e add
Rem DNeg, 459
461 ~(x,s(y),z') e n3 | EXIST(d):~~[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g)
e d => (e,s(f),s(g))
e d]
& ~(x,s(y),z')
e d] => ~(x,s(y),z')
e add
Imply-And, 460
Sufficient: ~(x,s(y),z') e add
462 ~(x,s(y),z') e n3 | EXIST(d):[d e pn3
& ALL(e):[e e n => (e,1,s(e)) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g)
e d => (e,s(f),s(g))
e d]
& ~(x,s(y),z')
e d] => ~(x,s(y),z')
e add
Rem DNeg, 461
463 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=> (a,b,c) e add & ~[a=x & b=s(y) & c=z']]]
Subset, 25
464 Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=> (a,b,c) e add & ~[a=x & b=s(y) & c=z']]
E Spec, 463
Define: q
*********
465 Set''(q)
Split, 464
466 ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=> (a,b,c) e add & ~[a=x & b=s(y) & c=z']]
Split, 464
Prove: ALL(e):[e e n => (e,1,s(e)) e q]
Suppose...
467 t e n
Premise
468 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e add & ~[t=x & b=s(y) & c=z']]
U Spec, 466
469 ALL(c):[(t,1,c) e q
<=> (t,1,c) e add & ~[t=x & 1=s(y) & c=z']]
U Spec, 468
470 (t,1,s(t)) e q
<=> (t,1,s(t)) e add & ~[t=x & 1=s(y) & s(t)=z']
U Spec, 469
471 [(t,1,s(t)) e q => (t,1,s(t)) e add & ~[t=x & 1=s(y) & s(t)=z']]
& [(t,1,s(t)) e add & ~[t=x & 1=s(y) & s(t)=z'] => (t,1,s(t)) e q]
Iff-And, 470
472 (t,1,s(t)) e q => (t,1,s(t)) e add & ~[t=x & 1=s(y) & s(t)=z']
Split, 471
Sufficient: (t,1,s(t)) e q
473 (t,1,s(t)) e add & ~[t=x & 1=s(y) & s(t)=z'] => (t,1,s(t)) e q
Split, 471
474 t e n => (t,1,s(t)) e add
U Spec, 54
475 (t,1,s(t)) e add
Detach, 474, 467
Prove: ~[t=x & 1=s(y) & s(t)=z']
Suppose to the contrary...
476 t=x & 1=s(y) & s(t)=z'
Premise
477 t=x
Split, 476
478 1=s(y)
Split, 476
479 s(t)=z'
Split, 476
480 y e n => ~s(y)=1
U Spec, 5
481 ALL(b):ALL(c):[(x,b,c) e add
=> (x,b,c) e n3 & [x e n & b e n & c e n]]
U Spec, 73
482 ALL(c):[(x,y,c) e add
=> (x,y,c) e n3 & [x e n & y e n & c e n]]
U Spec, 481
483 (x,y,z) e add
=> (x,y,z) e n3 & [x e n & y e n & z e n]
U Spec, 482
484 (x,y,z) e n3 & [x e n & y e n & z e n]
Detach, 483, 435
485 (x,y,z) e n3
Split, 484
486 x e n & y e n & z e n
Split, 484
487 x e n
Split, 486
488 y e n
Split, 486
489 z e n
Split, 486
490 ~s(y)=1
Detach, 480, 488
491 s(y)=1
Sym, 478
492 s(y)=1 & ~s(y)=1
Join, 491, 490
As Required:
493 ~[t=x & 1=s(y) & s(t)=z']
4 Conclusion, 476
494 (t,1,s(t)) e add & ~[t=x & 1=s(y) & s(t)=z']
Join, 475, 493
495 (t,1,s(t)) e q
Detach, 473, 494
As Required:
496 ALL(e):[e e n => (e,1,s(e)) e q]
4 Conclusion, 467
497
q
e pn3
<=> Set''(q)
& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3)
e q
=> (d1,d2,d3) e
n3]
U Spec, 22
498
[q
e pn3
=> Set''(q)
& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3)
e q
=> (d1,d2,d3) e
n3]]
& [Set''(q)
& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3)
e q
=> (d1,d2,d3) e
n3]
=> q
e pn3]
Iff-And, 497
499
q
e pn3
=> Set''(q)
& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3)
e q
=> (d1,d2,d3) e
n3]
Split, 498
500
Set''(q)
& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3)
e q
=> (d1,d2,d3) e
n3]
=> q
e pn3
Split, 498
Prove: ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Suppose...
501 (t,u,v) e q
Premise
502 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e add & ~[t=x & b=s(y) & c=z']]
U Spec, 466
503 ALL(c):[(t,u,c) e q
<=> (t,u,c) e add & ~[t=x & u=s(y) & c=z']]
U Spec, 502
504 (t,u,v) e q
<=> (t,u,v) e add & ~[t=x & u=s(y) & v=z']
U Spec, 503
505 [(t,u,v) e q => (t,u,v) e add & ~[t=x & u=s(y) & v=z']]
& [(t,u,v) e add & ~[t=x & u=s(y) & v=z'] => (t,u,v) e q]
Iff-And, 504
506 (t,u,v) e q => (t,u,v) e add & ~[t=x & u=s(y) & v=z']
Split, 505
507 (t,u,v) e add & ~[t=x & u=s(y) & v=z'] => (t,u,v) e q
Split, 505
508 (t,u,v) e add & ~[t=x & u=s(y) & v=z']
Detach, 506, 501
509 (t,u,v) e add
Split, 508
510 ~[t=x & u=s(y) & v=z']
Split, 508
511 ALL(b):ALL(c):[(t,b,c) e add
=> (t,b,c) e n3 & [t e n & b e n & c e n]]
U Spec, 73
512 ALL(c):[(t,u,c) e add
=> (t,u,c) e n3 & [t e n & u e n & c e n]]
U Spec, 511
513 (t,u,v) e add
=> (t,u,v) e n3 & [t e n & u e n & v e n]
U Spec, 512
514 (t,u,v) e n3 & [t e n & u e n & v e n]
Detach, 513, 509
515 (t,u,v) e n3
Split, 514
As Required:
516 ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
4 Conclusion, 501
517 Set''(q)
& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Join, 465, 516
As Required:
518 q e pn3
Detach, 500, 517
Prove: ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,s(f),s(g)) e q]
Suppose...
519 (t,u,v) e q
Premise
520 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e add & ~[t=x & b=s(y) & c=z']]
U Spec, 466
521 ALL(c):[(t,s(u),c) e q
<=> (t,s(u),c) e add & ~[t=x & s(u)=s(y) & c=z']]
U Spec, 520
522 (t,s(u),s(v)) e q
<=> (t,s(u),s(v)) e add & ~[t=x & s(u)=s(y) & s(v)=z']
U Spec, 521
523
[(t,s(u),s(v))
e q
=> (t,s(u),s(v))
e add
& ~[t=x
& s(u)=s(y)
& s(v=z']]
& [(t,s(u),s(v))
e add
& ~[t=x
& s(u)=s(y)
& s(v)=z']
=> (t,s(u),s(v))
e q]
Iff-And, 522
524
(t,s(u),s(v))
e q
=> (t,s(u),s(v))
e add
& ~[t=x
& s(u)=s(y)
& s(v)=z']
Split, 523
Sufficient: For (t,s(u),s(v)) e q
525
(t,s(u),s(v))
e add
& ~[t=x
& s(u)=s(y)
& s(v)=z']
=> (t,s(u),s(v))
e q
Split, 523
526 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e add & ~[t=x & b=s(y) & c=z']]
U Spec, 466
527 ALL(c):[(t,u,c) e q
<=> (t,u,c) e add & ~[t=x & u=s(y) & c=z']]
U Spec, 526
528 (t,u,v) e q
<=> (t,u,v) e add & ~[t=x & u=s(y) & v=z']
U Spec, 527
529 [(t,u,v) e q => (t,u,v) e add & ~[t=x & u=s(y) & v=z']]
& [(t,u,v) e add & ~[t=x & u=s(y) & v=z'] => (t,u,v) e q]
Iff-And, 528
530 (t,u,v) e q => (t,u,v) e add & ~[t=x & u=s(y) & v=z']
Split, 529
531 (t,u,v) e add & ~[t=x & u=s(y) & v=z'] => (t,u,v) e q
Split, 529
532 (t,u,v) e add & ~[t=x & u=s(y) & v=z']
Detach, 530, 519
533 (t,u,v) e add
Split, 532
534 ~[t=x & u=s(y) & v=z']
Split, 532
535 ALL(b):ALL(c):[(t,b,c) e add => (t,s(b),s(c)) e add]
U Spec, 125
536 ALL(c):[(t,u,c) e add => (t,s(u),s(c)) e add]
U Spec, 535
537 (t,u,v) e add => (t,s(u),s(v)) e add
U Spec, 536
538 (t,s(u),s(v)) e add
Detach, 537, 533
Prove: ~[t=x & s(u)=s(y) & s(v)=z']
Suppose to the contrary...
539 t=x & s(u)=s(y) & s(v)=z'
Premise
540 t=x
Split, 539
541 s(u)=s(y)
Split, 539
542 s(v)=z'
Split, 539
543 ALL(b):[u e n & b e n => [s(u)=s(b) => u=b]]
U Spec, 4
544 u e n & y e n => [s(u)=s(y) => u=y]
U Spec, 543
545 ALL(b):ALL(c):[(t,b,c) e add
=> (t,b,c) e n3 & [t e n & b e n & c e n]]
U Spec, 73
546 ALL(c):[(t,u,c) e add
=> (t,u,c) e n3 & [t e n & u e n & c e n]]
U Spec, 545
547 (t,u,v) e add
=> (t,u,v) e n3 & [t e n & u e n & v e n]
U Spec, 546
548 (t,u,v) e n3 & [t e n & u e n & v e n]
Detach, 547, 533
549 (t,u,v) e n3
Split, 548
550 t e n & u e n & v e n
Split, 548
551 t e n
Split, 550
552 u e n
Split, 550
553 v e n
Split, 550
554 u e n & y e n
Join, 552, 421
555 s(u)=s(y) => u=y
Detach, 544, 554
556 u=y
Detach, 555, 541
557 (x,u,v) e add
Substitute, 540, 533
558 (x,y,v) e add
Substitute, 556, 557
559 v e n => [(x,y,v) e add => z=v]
U Spec, 443
560 (x,y,v) e add => z=v
Detach, 559, 553
561 z=v
Detach, 560, 558
562 s(z)=z'
Substitute, 561, 542
563 z'=s(z)
Sym, 562
564 z'=s(z) & ~z'=s(z)
Join, 563, 449
As Required:
565 ~[t=x & s(u)=s(y) & s(v)=z']
4 Conclusion, 539
566 (t,s(u),s(v)) e add
& ~[t=x & s(u)=s(y) & s(v)=z']
Join, 538, 565
567 (t,s(u),s(v)) e q
Detach, 525, 566
As Required:
568 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,s(f),s(g)) e q]
4 Conclusion, 519
569 ALL(b):ALL(c):[(x,b,c) e q
<=> (x,b,c) e add & ~[x=x & b=s(y) & c=z']]
U Spec, 466
570 ALL(c):[(x,s(y),c) e q
<=> (x,s(y),c) e add & ~[x=x & s(y)=s(y) & c=z']]
U Spec, 569
571 (x,s(y),z') e q
<=> (x,s(y),z') e add & ~[x=x & s(y)=s(y) & z'=z']
U Spec, 570
572 [(x,s(y),z') e q => (x,s(y),z') e add & ~[x=x & s(y)=s(y) & z'=z']]
& [(x,s(y),z') e add & ~[x=x & s(y)=s(y) & z'=z'] => (x,s(y),z') e q]
Iff-And, 571
573 (x,s(y),z') e q => (x,s(y),z') e add & ~[x=x & s(y)=s(y) & z'=z']
Split, 572
574 (x,s(y),z') e add & ~[x=x & s(y)=s(y) & z'=z'] => (x,s(y),z') e q
Split, 572
575 ~[(x,s(y),z') e add & ~[x=x & s(y)=s(y) & z'=z']] => ~(x,s(y),z') e q
Contra, 573
576 ~~[~(x,s(y),z') e add | ~~[x=x & s(y)=s(y) & z'=z']] => ~(x,s(y),z') e q
DeMorgan, 575
577 ~(x,s(y),z') e add | ~~[x=x & s(y)=s(y) & z'=z'] => ~(x,s(y),z') e q
Rem DNeg, 576
578 ~(x,s(y),z') e add | x=x & s(y)=s(y) & z'=z' => ~(x,s(y),z') e q
Rem DNeg, 577
579 x=x
Reflex
580 s(y)=s(y)
Reflex
581 z'=z'
Reflex
582 x=x & s(y)=s(y)
Join, 579, 580
583 x=x & s(y)=s(y) & z'=z'
Join, 582, 581
584 ~(x,s(y),z') e add | x=x & s(y)=s(y) & z'=z'
Arb Or, 583
As Required:
585 ~(x,s(y),z') e q
Detach, 578, 584
586 q e pn3 & ALL(e):[e e n => (e,1,s(e)) e q]
Join, 518, 496
587 q e pn3 & ALL(e):[e e n => (e,1,s(e)) e q]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,s(f),s(g)) e q]
Join, 586, 568
588 q e pn3 & ALL(e):[e e n => (e,1,s(e)) e q]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,s(f),s(g)) e q]
& ~(x,s(y),z') e q
Join, 587, 585
589 EXIST(d):[d e pn3 & ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
& ~(x,s(y),z') e d]
E Gen, 588
590 ~(x,s(y),z') e n3 | EXIST(d):[d e pn3 & ALL(e):[e e n => (e,1,s(e)) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
& ~(x,s(y),z') e d]
Arb Or, 589
591 ~(x,s(y),z') e add
Detach, 462, 590
592 (x,s(y),z') e add & ~(x,s(y),z') e add
Join, 448, 591
As Required:
593 ~[(x,s(y),z') e add & ~z'=s(z)]
4 Conclusion, 445
594 ~~[(x,s(y),z') e add => ~~z'=s(z)]
Imply-And, 593
595 (x,s(y),z') e add => ~~z'=s(z)
Rem DNeg, 594
596 (x,s(y),z') e add => z'=s(z)
Rem DNeg, 595
As Required:
597 ALL(c):[c e n => [(x,s(y),c) e add => c=s(z)]]
4 Conclusion, 444
Prove: ALL(c1):ALL(c2):[(x,s(y),c1) e add & (x,s(y),c2) e add => c1=c2]
Suppose...
598 (x,s(y),z1) e add & (x,s(y),z2) e add
Premise
599 (x,s(y),z1) e add
Split, 598
600 (x,s(y),z2) e add
Split, 598
601 z1 e n => [(x,s(y),z1) e add => z1=s(z)]
U Spec, 597
602 ALL(b):ALL(c):[(x,b,c) e add
=> (x,b,c) e n3 & [x e n & b e n & c e n]]
U Spec, 73
603 ALL(c):[(x,s(y),c) e add
=> (x,s(y),c) e n3 & [x e n & s(y) e n & c e n]]
U Spec, 602
604 (x,s(y),z1) e add
=> (x,s(y),z1) e n3 & [x e n & s(y) e n & z1 e n]
U Spec, 603
605 (x,s(y),z1) e n3 & [x e n & s(y) e n & z1 e n]
Detach, 604, 599
606 (x,s(y),z1) e n3
Split, 605
607 x e n & s(y) e n & z1 e n
Split, 605
608 x e n
Split, 607
609 s(y) e n
Split, 607
610 z1 e n
Split, 607
611 (x,s(y),z1) e add => z1=s(z)
Detach, 601, 610
612 z1=s(z)
Detach, 611, 599
613 z2 e n => [(x,s(y),z2) e add => z2=s(z)]
U Spec, 597
614 (x,s(y),z2) e add
=> (x,s(y),z2) e n3 & [x e n & s(y) e n & z2 e n]
U Spec, 603
615 (x,s(y),z2) e n3 & [x e n & s(y) e n & z2 e n]
Detach, 614, 600
616 (x,s(y),z2) e n3
Split, 615
617 x e n & s(y) e n & z2 e n
Split, 615
618 x e n
Split, 617
619 s(y) e n
Split, 617
620 z2 e n
Split, 617
621 (x,s(y),z2) e add => z2=s(z)
Detach, 613, 620
622 z2=s(z)
Detach, 621, 600
623 z1=z2
Substitute, 622, 612
As Required:
624 ALL(c1):ALL(c2):[(x,s(y),c1) e add & (x,s(y),c2) e add => c1=c2]
4 Conclusion, 598
625 s(y) e n
& ALL(c1):ALL(c2):[(x,s(y),c1) e add & (x,s(y),c2) e add => c1=c2]
Join, 428, 624
626 s(y) e r
Detach, 426, 625
As Required:
627 ALL(b):[b e r => s(b) e r]
4 Conclusion, 415
628 1 e r & ALL(b):[b e r => s(b) e r]
Join, 414, 627
As Required:
629 ALL(b):[b e n => b e r]
Detach, 378, 628
Prove: ALL(b):[b e n
=> ALL(c1):ALL(c2):[(x,b,c1) e add & (x,b,c2) e add => c1=c2]]
Suppose...
630 y e n
Premise
631 y e n => y e r
U Spec, 629
632 y e r
Detach, 631, 630
633 y e r <=> y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2]
U Spec, 367
634 [y e r => y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2]]
& [y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2] => y e r]
Iff-And, 633
635 y e r => y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2]
Split, 634
636 y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2] => y e r
Split, 634
637 y e n & ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2]
Detach, 635, 632
638 y e n
Split, 637
639 ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2]
Split, 637
As Required:
640 ALL(b):[b e n
=> ALL(c1):ALL(c2):[(x,b,c1) e add & (x,b,c2) e add => c1=c2]]
4 Conclusion, 630
As Required:
641 ALL(a):[a e n
=> ALL(b):[b e n
=> ALL(c1):ALL(c2):[(a,b,c1) e add & (a,b,c2) e add => c1=c2]]]
4 Conclusion, 363
Prove: ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]
Suppose...
642 (x,y,z1) e add & (x,y,z2) e add
Premise
643 (x,y,z1) e add
Split, 642
644 (x,y,z2) e add
Split, 642
645 ALL(b):ALL(c):[(x,b,c) e add
=> (x,b,c) e n3 & [x e n & b e n & c e n]]
U Spec, 73
646 ALL(c):[(x,y,c) e add
=> (x,y,c) e n3 & [x e n & y e n & c e n]]
U Spec, 645
647 (x,y,z1) e add
=> (x,y,z1) e n3 & [x e n & y e n & z1 e n]
U Spec, 646
648 (x,y,z1) e n3 & [x e n & y e n & z1 e n]
Detach, 647, 643
649 (x,y,z1) e n3
Split, 648
650 x e n & y e n & z1 e n
Split, 648
651 x e n
Split, 650
652 y e n
Split, 650
653 z1 e n
Split, 650
654 x e n
=> ALL(b):[b e n
=> ALL(c1):ALL(c2):[(x,b,c1) e add & (x,b,c2) e add => c1=c2]]
U Spec, 641
655 ALL(b):[b e n
=> ALL(c1):ALL(c2):[(x,b,c1) e add & (x,b,c2) e add => c1=c2]]
Detach, 654, 651
656 y e n
=> ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2]
U Spec, 655
657 ALL(c1):ALL(c2):[(x,y,c1) e add & (x,y,c2) e add => c1=c2]
Detach, 656, 652
658 ALL(c2):[(x,y,z1) e add & (x,y,c2) e add => z1=c2]
U Spec, 657
659 (x,y,z1) e add & (x,y,z2) e add => z1=z2
U Spec, 658
660 z1=z2
Detach, 659, 642
Functionality of add: Part 3
As Required:
661 ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]
4 Conclusion, 642
662 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => c1 e n & c2 e n & d e n]
& ALL(c1):ALL(c2):[c1 e n & c2 e n => EXIST(b):[b e n & (c1,c2,b) e add]]
Join, 282, 362
663 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => c1 e n & c2 e n & d e n]
& ALL(c1):ALL(c2):[c1 e n & c2 e n => EXIST(b):[b e n & (c1,c2,b) e add]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]
Join, 662, 661
As Required: add is a function
664 ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) e add]
Detach, 274, 663
Prove: ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
Suppose...
665 x e n & y e n
Premise
666 x e n
Split, 665
667 y e n
Split, 665
668 ALL(c2):[x e n & c2 e n => EXIST(b):[b e n & (x,c2,b) e add]]
U Spec, 362
669 x e n & y e n => EXIST(b):[b e n & (x,y,b) e add]
U Spec, 668
670 EXIST(b):[b e n & (x,y,b) e add]
Detach, 669, 665
671 z e n & (x,y,z) e add
E Spec, 670
672 z e n
Split, 671
673 (x,y,z) e add
Split, 671
674 ALL(c2):ALL(d):[d=add(x,c2) <=> (x,c2,d) e add]
U Spec, 664
675 ALL(d):[d=add(x,y) <=> (x,y,d) e add]
U Spec, 674
676 z=add(x,y) <=> (x,y,z) e add
U Spec, 675
677 [z=add(x,y) => (x,y,z) e add]
& [(x,y,z) e add => z=add(x,y)]
Iff-And, 676
678 z=add(x,y) => (x,y,z) e add
Split, 677
679 (x,y,z) e add => z=add(x,y)
Split, 677
680 z=add(x,y)
Detach, 679, 673
681 add(x,y) e n
Substitute, 680, 672
As Required:
682 ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
4 Conclusion, 665
Prove: ALL(a):[a e n => add(a,1)=s(a)]
Suppose...
683 x e n
Premise
684 x e n => (x,1,s(x)) e add
U Spec, 54
685 (x,1,s(x)) e add
Detach, 684, 683
686 ALL(c2):ALL(d):[d=add(x,c2) <=> (x,c2,d) e add]
U Spec, 664
687 ALL(d):[d=add(x,1) <=> (x,1,d) e add]
U Spec, 686
688 s(x)=add(x,1) <=> (x,1,s(x)) e add
U Spec, 687
689 [s(x)=add(x,1) => (x,1,s(x)) e add]
& [(x,1,s(x)) e add => s(x)=add(x,1)]
Iff-And, 688
690 s(x)=add(x,1) => (x,1,s(x)) e add
Split, 689
691 (x,1,s(x)) e add => s(x)=add(x,1)
Split, 689
692 s(x)=add(x,1)
Detach, 691, 685
693 add(x,1)=s(x)
Sym, 692
As Required:
694 ALL(a):[a e n => add(a,1)=s(a)]
4 Conclusion, 683
Prove: ALL(a):ALL(b):[a e n & b e n => add(a,s(b))=s(add(a,b))]
Suppose...
695 x e n & y e n
Premise
696 x e n
Split, 695
697 y e n
Split, 695
698 ALL(c2):[x e n & c2 e n => EXIST(b):[b e n & (x,c2,b) e add]]
U Spec, 362
699 x e n & y e n => EXIST(b):[b e n & (x,y,b) e add]
U Spec, 698
700 EXIST(b):[b e n & (x,y,b) e add]
Detach, 699, 695
701 z e n & (x,y,z) e add
E Spec, 700
702 z e n
Split, 701
703 (x,y,z) e add
Split, 701
704 ALL(c2):ALL(d):[d=add(x,c2) <=> (x,c2,d) e add]
U Spec, 664
705 ALL(d):[d=add(x,y) <=> (x,y,d) e add]
U Spec, 704
706 z=add(x,y) <=> (x,y,z) e add
U Spec, 705
707 [z=add(x,y) => (x,y,z) e add]
& [(x,y,z) e add => z=add(x,y)]
Iff-And, 706
708 z=add(x,y) => (x,y,z) e add
Split, 707
709 (x,y,z) e add => z=add(x,y)
Split, 707
710 z=add(x,y)
Detach, 709, 703
711 ALL(b):ALL(c):[(x,b,c) e add => (x,s(b),s(c)) e add]
U Spec, 125
712 ALL(c):[(x,y,c) e add => (x,s(y),s(c)) e add]
U Spec, 711
713 (x,y,z) e add => (x,s(y),s(z)) e add
U Spec, 712
714 (x,s(y),s(z)) e add
Detach, 713, 703
715 ALL(c2):ALL(d):[d=add(x,c2) <=> (x,c2,d) e add]
U Spec, 664
716 ALL(d):[d=add(x,s(y)) <=> (x,s(y),d) e add]
U Spec, 715
717 s(z)=add(x,s(y)) <=> (x,s(y),s(z)) e add
U Spec, 716
718 [s(z)=add(x,s(y)) => (x,s(y),s(z)) e add]
& [(x,s(y),s(z)) e add => s(z)=add(x,s(y))]
Iff-And, 717
719 s(z)=add(x,s(y)) => (x,s(y),s(z)) e add
Split, 718
720 (x,s(y),s(z)) e add => s(z)=add(x,s(y))
Split, 718
721 s(z)=add(x,s(y))
Detach, 720, 714
722 s(add(x,y))=add(x,s(y))
Substitute, 710, 721
723 add(x,s(y))=s(add(x,y))
Sym, 722
As Required:
724 ALL(a):ALL(b):[a e n & b e n => add(a,s(b))=s(add(a,b))]
4 Conclusion, 695
725 ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
& ALL(a):[a e n => add(a,1)=s(a)]
Join, 682, 694
726 ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
& ALL(a):[a e n => add(a,1)=s(a)]
& ALL(a):ALL(b):[a e n & b e n => add(a,s(b))=s(add(a,b))]
Join, 725, 724
As Required:
727 EXIST(add):[ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
& ALL(a):[a e n => add(a,1)=s(a)]
& ALL(a):ALL(b):[a e n & b e n => add(a,s(b))=s(add(a,b))]]
E Gen, 726