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