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) 
	& 1n 
	& 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