Constructing the MULTIPLY Function
Here, we construct the multiply function for the natural numbers using Peano's
Axioms and previous results for the add function (+).
(F5 to view highlights only)
Peano's axioms for the natural numbers
1 Set(n)
& 1
n
& ALL(a):[an => next(a)n]
& ALL(a):[an => ~next(a)=1]
& ALL(a):ALL(b):[an & bn & next(a)=next(b) => a=b]
& ALL(a):[Set(a) & 1a & ALL(b):[bn & ba => next(b)a]
=> ALL(b):[bn => ba]]
Premise
Splitting...
2 Set(n)
Split, 1
3 1n
Split, 1
4 ALL(a):[an => next(a)n]
Split, 1
5 ALL(a):[an => ~next(a)=1]
Split, 1
6 ALL(a):ALL(b):[an & bn & next(a)=next(b) => a=b]
Split, 1
7 ALL(a):[Set(a) & 1a & ALL(b):[bn & ba => next(b)a]
=> ALL(b):[bn => ba]]
Split, 1
Define: + for the natural numbers
8 ALL(a):ALL(b):[an & bn => a+bn]
& ALL(a):[an => a+1=next(a)]
& ALL(a):ALL(b):[an & bn => a+next(b)=next(a+b)]
Definition
9 ALL(a):ALL(b):[an & bn => a+bn]
Split, 8
10 ALL(a):[an => a+1=next(a)]
Split, 8
11 ALL(a):ALL(b):[an & bn => a+next(b)=next(a+b)]
Split, 8
Properties of + (previous results)
12 ALL(a):ALL(b):ALL(c):[an & bn & cn => a+b+c=a+(b+c)]
& ALL(a):ALL(b):[an & bn => a+b=b+a]
& ALL(a):ALL(b):ALL(c):[an & bn & cn & a+b=c+b => a=c]
Premise
+ is associative
13 ALL(a):ALL(b):ALL(c):[an & bn & cn => a+b+c=a+(b+c)]
Split, 12
+ is commutative
14 ALL(a):ALL(b):[an & bn => a+b=b+a]
Split, 12
+ is cancellable
15 ALL(a):ALL(b):ALL(c):[an & bn & cn & a+b=c+b => a=c]
Split, 12
Construct the set of ordered triples of natural numbers, n3
Applying the Cartesian Product rule...
16 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)b <=> c1a1 & c2a2 & c3a3]]]
Cart Prod
17 ALL(a2):ALL(a3):[Set(n) & Set(a2) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)b <=> c1n & c2a2 & c3a3]]]
U Spec, 16
18 ALL(a3):[Set(n) & Set(n) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)b <=> c1n & c2n & c3a3]]]
U Spec, 17
19 Set(n) & Set(n) & Set(n) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)b <=> c1n & c2n & c3n]]
U Spec, 18
20 Set(n) & Set(n)
Join, 2, 2
21 Set(n) & Set(n) & Set(n)
Join, 20, 2
22 EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)b <=> c1n & c2n & c3n]]
Detach, 19, 21
Define: n3, the set of ordered triples of natural numbers
23 Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)n3 <=> c1n & c2n & c3n]
E Spec, 22
24 Set''(n3)
Split, 23
25 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)n3 <=> c1n & c2n & c3n]
Split, 23
26 EXIST(multiply):[Set''(multiply) & ALL(a):ALL(b):ALL(c):[(a,b,c)multiply
<=> (a,b,c)n3 & [b=1 & c=a | EXIST(b'):EXIST(c'):[b'n & c'n & (a,b',c')multiply & b=b'+1 & c=c'+a]]]]
Subset, 24
Define: multiply, a subset of n3
27 Set''(multiply) & ALL(a):ALL(b):ALL(c):[(a,b,c)multiply
<=> (a,b,c)n3 & [b=1 & c=a | EXIST(b'):EXIST(c'):[b'n & c'n & (a,b',c')multiply & b=b'+1 & c=c'+a]]]
E Spec, 26
28 Set''(multiply)
Split, 27
29 ALL(a):ALL(b):ALL(c):[(a,b,c)multiply
<=> (a,b,c)n3 & [b=1 & c=a | EXIST(b'):EXIST(c'):[b'n & c'n & (a,b',c')multiply & b=b'+1 & c=c'+a]]]
Split, 27
Prove: xn => (x,1,x) mulitply
Suppose...
30 xn
Premise
31 ALL(b):ALL(c):[(x,b,c)multiply
<=> (x,b,c)n3 & [b=1 & c=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & b=b'+1 & c=c'+x]]]
U Spec, 29
32 ALL(c):[(x,1,c)multiply
<=> (x,1,c)n3 & [1=1 & c=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & 1=b'+1 & c=c'+x]]]
U Spec, 31
33 (x,1,x)multiply
<=> (x,1,x)n3 & [1=1 & x=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & 1=b'+1 & x=c'+x]]
U Spec, 32
34 [(x,1,x)multiply => (x,1,x)n3 & [1=1 & x=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & 1=b'+1 & x=c'+x]]]
& [(x,1,x)n3 & [1=1 & x=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & 1=b'+1 & x=c'+x]] => (x,1,x)multiply]
Iff-And, 33
35 (x,1,x)multiply => (x,1,x)n3 & [1=1 & x=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & 1=b'+1 & x=c'+x]]
Split, 34
Sufficient: For (x,1,x) multiply
36 (x,1,x)n3 & [1=1 & x=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & 1=b'+1 & x=c'+x]] => (x,1,x)multiply
Split, 34
Prove: (x,1,x)n3
37 ALL(c2):ALL(c3):[(x,c2,c3)n3 <=> xn & c2n & c3n]
U Spec, 25
38 ALL(c3):[(x,1,c3)n3 <=> xn & 1n & c3n]
U Spec, 37
39 (x,1,x)n3 <=> xn & 1n & xn
U Spec, 38
40 [(x,1,x)n3 => xn & 1n & xn]
& [xn & 1n & xn => (x,1,x)n3]
Iff-And, 39
41 (x,1,x)n3 => xn & 1n & xn
Split, 40
42 xn & 1n & xn => (x,1,x)n3
Split, 40
43 xn & 1n
Join, 30, 3
44 xn & 1n & xn
Join, 43, 30
As Required:
45 (x,1,x)n3
Detach, 42, 44
46 1=1
Reflex
47 x=x
Reflex
48 1=1 & x=x
Join, 46, 47
49 1=1 & x=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & 1=b'+1 & x=c'+x]
Arb Or, 48
50 (x,1,x)n3
& [1=1 & x=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & 1=b'+1 & x=c'+x]]
Join, 45, 49
51 (x,1,x)multiply
Detach, 36, 50
As Required:
52 xn => (x,1,x)multiply
Conclusion, 30
Lemma 1
53 ALL(a):[an => (a,1,a)multiply]
U Gen, 52
Prove: xn & yn & zn & (x,y,z)multiply => (x,y+1,z+x) multiply
Suppose...
54 xn & yn & zn & (x,y,z)multiply
Premise
55 xn
Split, 54
56 yn
Split, 54
57 zn
Split, 54
58 (x,y,z)multiply
Split, 54
59 ALL(b):ALL(c):[(x,b,c)multiply
<=> (x,b,c)n3 & [b=1 & c=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & b=b'+1 & c=c'+x]]]
U Spec, 29
60 ALL(c):[(x,y+1,c)multiply
<=> (x,y+1,c)n3 & [y+1=1 & c=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & y+1=b'+1 & c=c'+x]]]
U Spec, 59
61 (x,y+1,z+x)multiply
<=> (x,y+1,z+x)n3 & [y+1=1 & z+x=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & y+1=b'+1 & z+x=c'+x]]
U Spec, 60
62 [(x,y+1,z+x)multiply => (x,y+1,z+x)n3 & [y+1=1 & z+x=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & y+1=b'+1 & z+x=c'+x]]]
& [(x,y+1,z+x)n3 & [y+1=1 & z+x=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & y+1=b'+1 & z+x=c'+x]] => (x,y+1,z+x)multiply]
Iff-And, 61
63 (x,y+1,z+x)multiply => (x,y+1,z+x)n3 & [y+1=1 & z+x=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & y+1=b'+1 & z+x=c'+x]]
Split, 62
Sufficient: For (x,y+1,z+x) multiply
64 (x,y+1,z+x)n3 & [y+1=1 & z+x=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & y+1=b'+1 & z+x=c'+x]] => (x,y+1,z+x)multiply
Split, 62
Prove: (x,y+1,z+x)n3
65 ALL(c2):ALL(c3):[(x,c2,c3)n3 <=> xn & c2n & c3n]
U Spec, 25
66 ALL(c3):[(x,y+1,c3)n3 <=> xn & y+1n & c3n]
U Spec, 65
67 (x,y+1,z+x)n3 <=> xn & y+1n & z+xn
U Spec, 66
68 [(x,y+1,z+x)n3 => xn & y+1n & z+xn]
& [xn & y+1n & z+xn => (x,y+1,z+x)n3]
Iff-And, 67
69 (x,y+1,z+x)n3 => xn & y+1n & z+xn
Split, 68
70 xn & y+1n & z+xn => (x,y+1,z+x)n3
Split, 68
71 ALL(b):[yn & bn => y+bn]
U Spec, 9
72 yn & 1n => y+1n
U Spec, 71
73 yn & 1n
Join, 56, 3
74 y+1n
Detach, 72, 73
75 ALL(b):[zn & bn => z+bn]
U Spec, 9
76 zn & xn => z+xn
U Spec, 75
77 zn & xn
Join, 57, 55
78 z+xn
Detach, 76, 77
79 xn & y+1n
Join, 55, 74
80 xn & y+1n & z+xn
Join, 79, 78
As Required:
81 (x,y+1,z+x)n3
Detach, 70, 80
82 y+1=y+1
Reflex
83 z+x=z+x
Reflex
84 yn & zn
Join, 56, 57
85 yn & zn & (x,y,z)multiply
Join, 84, 58
86 yn & zn & (x,y,z)multiply & y+1=y+1
Join, 85, 82
87 yn & zn & (x,y,z)multiply & y+1=y+1 & z+x=z+x
Join, 86, 83
88 EXIST(c'):[yn & c'n & (x,y,c')multiply & y+1=y+1 & z+x=c'+x]
E Gen, 87
89 EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & y+1=b'+1 & z+x=c'+x]
E Gen, 88
90 y+1=1 & z+x=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & y+1=b'+1 & z+x=c'+x]
Arb Or, 89
91 (x,y+1,z+x)n3
& [y+1=1 & z+x=x | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')multiply & y+1=b'+1 & z+x=c'+x]]
Join, 81, 90
92 (x,y+1,z+x)multiply
Detach, 64, 91
As Required:
93 xn & yn & zn & (x,y,z)multiply
=> (x,y+1,z+x)multiply
Conclusion, 54
94 ALL(c):[xn & yn & cn & (x,y,c)multiply
=> (x,y+1,c+x)multiply]
U Gen, 93
95 ALL(b):ALL(c):[xn & bn & cn & (x,b,c)multiply
=> (x,b+1,c+x)multiply]
U Gen, 94
Lemma 2
96 ALL(a):ALL(b):ALL(c):[an & bn & cn & (a,b,c)multiply
=> (a,b+1,c+a)multiply]
U Gen, 95
97 ALL(f):ALL(a1):ALL(a2):ALL(b):[Set''(f)
& Set(a1) & Set(a2) & Set(b)
& ALL(c1):ALL(c2):[c1a1 & c2a2 => EXIST(d):[db & (c1,c2,d)f]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1a1 & c2a2 & d1b & d2b & (c1,c2,d1)f & (c1,c2,d2)f => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[c1a1 & c2a2 & db => [d=f(c1,c2) <=> (c1,c2,d)f]]]
Function
98 ALL(a1):ALL(a2):ALL(b):[Set''(multiply)
& Set(a1) & Set(a2) & Set(b)
& ALL(c1):ALL(c2):[c1a1 & c2a2 => EXIST(d):[db & (c1,c2,d)multiply]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1a1 & c2a2 & d1b & d2b & (c1,c2,d1)multiply & (c1,c2,d2)multiply => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[c1a1 & c2a2 & db => [d=multiply(c1,c2) <=> (c1,c2,d)multiply]]]
U Spec, 97
99 ALL(a2):ALL(b):[Set''(multiply)
& Set(n) & Set(a2) & Set(b)
& ALL(c1):ALL(c2):[c1n & c2a2 => EXIST(d):[db & (c1,c2,d)multiply]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1n & c2a2 & d1b & d2b & (c1,c2,d1)multiply & (c1,c2,d2)multiply => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[c1n & c2a2 & db => [d=multiply(c1,c2) <=> (c1,c2,d)multiply]]]
U Spec, 98
100 ALL(b):[Set''(multiply)
& Set(n) & Set(n) & Set(b)
& ALL(c1):ALL(c2):[c1n & c2n => EXIST(d):[db & (c1,c2,d)multiply]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1n & c2n & d1b & d2b & (c1,c2,d1)multiply & (c1,c2,d2)multiply => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[c1n & c2n & db => [d=multiply(c1,c2) <=> (c1,c2,d)multiply]]]
U Spec, 99
Sufficient: For functionality of multiply
101 Set''(multiply)
& Set(n) & Set(n) & Set(n)
& ALL(c1):ALL(c2):[c1n & c2n => EXIST(d):[dn & (c1,c2,d)multiply]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1n & c2n & d1n & d2n & (c1,c2,d1)multiply & (c1,c2,d2)multiply => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[c1n & c2n & dn => [d=multiply(c1,c2) <=> (c1,c2,d)multiply]]
U Spec, 100