THEOREM
*******
Constructing the partial function add, we prove:
EXIST(add):[ALL(a):[a e n => add(a,0)=a]
& ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & s(b) e n & s(c) e n
=> [add(a,b)=c => add(a,s(b))=s(c)]]]
Dan Christensen
Revised: 2014-04-24
This proof was written with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com
Axiom for partial functions of 2 variables giving the sufficient condition for the partial functionality of
a set of ordered triples.
1 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):ALL(d1):ALL(d2):[(c1,c2,d1) e f & (c1,c2,d2) e f => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[c1 e a1 & c2 e a2 & d e b => [f(c1,c2)=d <=> (c1,c2,d) e f]]]
Axiom
The Axioms for Finite Arithmetic
********************************
For a formal development of these axioms from s as a set of ordered pairs, see Finite Succession
2 Set(n)
Axiom
3 0 e n
Axiom
4 max e n
Axiom
All non-max elements have a successor
5 ALL(a):[a e n => [~a=max => s(a) e n]]
Axiom
max has no successor
6 ~s(max) e n
Axiom
0 has no predecessor
7 ALL(a):[a e n => ~s(a)=0]
Axiom
Predecessors are unique
8 ALL(a):ALL(b):[a e n & b e n & s(a) e n => [s(a)=s(b) => a=b]]
Axiom
Finite Induction
9 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a & s(b) e n => s(b) e a]
=> ALL(b):[b e n => b e a]]]
Axiom
Construct n3, the set of order triples of n
10 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
11 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, 10
12 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, 11
13 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, 12
14 Set(n) & Set(n)
Join, 2, 2
15 Set(n) & Set(n) & Set(n)
Join, 14, 2
16 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, 13, 15
17 Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
E Spec, 16
Define: n3
**********
18 Set''(n3)
Split, 17
19 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
Split, 17
Construct add, a subset of n3
Apply Subset Axiom
20 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 & s(f) e n & s(g) e n => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d]]]
Subset, 18
21 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 & s(f) e n & s(g) e n => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d]]
E Spec, 20
Define: add
***********
22 Set''(add)
Split, 21
23 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 & s(f) e n & s(g) e n => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d]]
Split, 21
24 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):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[c1 e a1 & c2 e a2 & d e b => [add(c1,c2)=d <=> (c1,c2,d) e add]]]
U Spec, 1
25 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):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[c1 e n & c2 e a2 & d e b => [add(c1,c2)=d <=> (c1,c2,d) e add]]]
U Spec, 24
26 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):ALL(d1):ALL(d2):[(c1,c2,d1) e add & (c1,c2,d2) e add => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[c1 e n & c2 e n & d e b => [add(c1,c2)=d <=> (c1,c2,d) e add]]]
U Spec, 25
Sufficient for partial functionality of add
27 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e add => c1 e n & c2 e n & d e n]
& 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):[c1 e n & c2 e n & d e n => [add(c1,c2)=d <=> (c1,c2,d) e add]]
U Spec, 26
As Required:
45 ALL(a):ALL(b):ALL(c):[(a,b,c) e add => a e n & b e n & c e n]
5 Conclusion, 28
Necessary for (a,b,c) e add
56 ALL(a):ALL(b):ALL(c):[(a,b,c) e add
=> 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 & s(f) e n & s(g) e n => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d]]
5 Conclusion, 46
Sufficient: For (a,b,c) e add
75 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n
=> [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 & s(f) e n & s(g) e n => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d]
=> (a,b,c) e add]]
5 Conclusion, 57
76 ALL(a):ALL(b):ALL(c):[~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 & s(f) e n & s(g) e n => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d] => ~(a,b,c) e add]
Contra, 56
77 ALL(a):ALL(b):ALL(c):[~~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 & s(f) e n & s(g) e n => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d] => ~(a,b,c) e add]
Quant, 76
78 ALL(a):ALL(b):ALL(c):[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 & s(f) e n & s(g) e n => [(e,f,g) e d => (e,s(f),s(g)) e d]]
=> (a,b,c) e d] => ~(a,b,c) e add]
Rem DNeg, 77
79 ALL(a):ALL(b):ALL(c):[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 & s(f) e n & s(g) e n => [(e,f,g) e d => (e,s(f),s(g)) e d]] & ~(a,b,c) e d] => ~(a,b,c) e add]
Imply-And, 78
Sufficient for ~(a,b,c) e add
80 ALL(a):ALL(b):ALL(c):[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 & s(f) e n & s(g) e n => [(e,f,g) e d => (e,s(f),s(g)) e d]] & ~(a,b,c) e d] => ~(a,b,c) e add]
Rem DNeg, 79
As Required:
97 ALL(a):[a e n => (a,0,a) e add]
5 Conclusion, 81
As Required:
134 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & s(b) e n & s(c) e n
=> [(a,b,c) e add => (a,s(b),s(c)) e add]]
5 Conclusion, 98
As Required:
250 ALL(a):ALL(c):[a e n & c e n => [(a,0,c) e add => c=a]]
5 Conclusion, 135
As Required:
439 ALL(a):[a e n
=> ALL(b):[b e n
=> EXIST(c):ALL(d):[d e n => [(a,b,d) e add => d=c]]]]
5 Conclusion, 251
As Required:
467 ALL(a):ALL(b):ALL(c):ALL(d):[(a,b,c) e add & (a,b,d) e add => c=d]
5 Conclusion, 440
468 ALL(a):ALL(b):ALL(c):[(a,b,c) e add => a e n & b e n & c e n]
& ALL(a):ALL(b):ALL(c):ALL(d):[(a,b,c) e add & (a,b,d) e add => c=d]
Join, 45, 467
add is a partial function
469 ALL(c1):ALL(c2):ALL(d):[c1 e n & c2 e n & d e n => [add(c1,c2)=d <=> (c1,c2,d) e add]]
Detach, 27, 468
As Required:
483 ALL(a):[a e n => add(a,0)=a]
5 Conclusion, 470
As Required:
517 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & s(b) e n & s(c) e n
=> [add(a,b)=c => add(a,s(b))=s(c)]]
5 Conclusion, 484
518 ALL(a):[a e n => add(a,0)=a]
& ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & s(b) e n & s(c) e n
=> [add(a,b)=c => add(a,s(b))=s(c)]]
Join, 483, 517
As Required:
519 EXIST(add):[ALL(a):[a e n => add(a,0)=a]
& ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & s(b) e n & s(c) e n
=> [add(a,b)=c => add(a,s(b))=s(c)]]]
E Gen, 518