Constructing the ADD Function

Introduction

(Key F5 to view the highlights -- in DC Proof only)

Here is the beginning of a proof to construct the ADD function for the
natural numbers. It is the first installment of a series of proofs to 
construct the real numbers from Peano's Axioms.  

Required to Prove: As constructed below, prove that set add is a function.

We begin by constructing the set of orders triples of the natural numbers, n3.
Then we select a subset 'add' from n3. We want to prove that 'add' is a 
function. Here, I have used proof by induction to show that

xn & yn => EXIST(z):[zn & (x,y,z)add]

To prove that 'add' is a function, you must also prove (by induction) 
that 

(x,y,z1)add & (x,y,z2)add => z1=z2

Then you will be able to conclude that 

z=add(x,y) <=> (x,y,z)add


Peano's axioms for the natural numbers (from Numbers menu)

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

Construct the set of ordered triples of natural numbers, n3

Applying the Cartesian Product rule...

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)b <=> c1a1 & c2a2 & c3a3]]]
	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)b <=> c1n & c2a2 & c3a3]]]
	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)b <=> c1n & c2n & c3a3]]]
	U Spec, 9

11	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, 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)b <=> c1n & c2n & c3n]]
	Detach, 11, 13

Define: n3, the set of ordered triples of natural numbers

15	Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)n3 <=> c1n & c2n & c3n]
	E Spec, 14

16	Set''(n3)
	Split, 15

17	ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3)n3 <=> c1n & c2n & c3n]
	Split, 15

Construct the add function, a subset of n3

Applying the Subset rule...

18	EXIST(s):[Set''(s) & ALL(a):ALL(b):ALL(c):[(a,b,c)s 
	<=> (a,b,c)n3 & [b=1 & next(a)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (a,b',c')s & next(b')=b & next(c')=c]]]]
	Subset, 16

Define: add, a subset of n3

19	Set''(add) & ALL(a):ALL(b):ALL(c):[(a,b,c)add 
	<=> (a,b,c)n3 & [b=1 & next(a)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (a,b',c')add & next(b')=b & next(c')=c]]]
	E Spec, 18

20	Set''(add)
	Split, 19

21	ALL(a):ALL(b):ALL(c):[(a,b,c)add 
	<=> (a,b,c)n3 & [b=1 & next(a)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (a,b',c')add & next(b')=b & next(c')=c]]]
	Split, 19

Prove: Add is a function

Applying the definiton of functionality...

22	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

23	ALL(a1):ALL(a2):ALL(b):[Set''(add) 
	& Set(a1) & Set(a2) & Set(b) 
	& ALL(c1):ALL(c2):[c1a1 & c2a2 => EXIST(d):[db & (c1,c2,d)add]] 
	& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1a1 & c2a2 & d1b & d2b & (c1,c2,d1)add & (c1,c2,d2)add => d1=d2] 
	=> ALL(c1):ALL(c2):ALL(d):[c1a1 & c2a2 & db => [d=add(c1,c2) <=> (c1,c2,d)add]]]
	U Spec, 22

24	ALL(a2):ALL(b):[Set''(add) 
	& Set(n) & Set(a2) & Set(b) 
	& ALL(c1):ALL(c2):[c1n & c2a2 => EXIST(d):[db & (c1,c2,d)add]] 
	& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1n & c2a2 & d1b & d2b & (c1,c2,d1)add & (c1,c2,d2)add => d1=d2] 
	=> ALL(c1):ALL(c2):ALL(d):[c1n & c2a2 & db => [d=add(c1,c2) <=> (c1,c2,d)add]]]
	U Spec, 23

25	ALL(b):[Set''(add) 
	& Set(n) & Set(n) & Set(b) 
	& ALL(c1):ALL(c2):[c1n & c2n => EXIST(d):[db & (c1,c2,d)add]] 
	& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1n & c2n & d1b & d2b & (c1,c2,d1)add & (c1,c2,d2)add => d1=d2] 
	=> ALL(c1):ALL(c2):ALL(d):[c1n & c2n & db => [d=add(c1,c2) <=> (c1,c2,d)add]]]
	U Spec, 24

Sufficient: For functionality of add

26	Set''(add) 
	& Set(n) & Set(n) & Set(n) 
	& ALL(c1):ALL(c2):[c1n & c2n => EXIST(d):[dn & (c1,c2,d)add]] 
	& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1n & c2n & d1n & d2n & (c1,c2,d1)add & (c1,c2,d2)add => d1=d2] 
	=> ALL(c1):ALL(c2):ALL(d):[c1n & c2n & dn => [d=add(c1,c2) <=> (c1,c2,d)add]]
	U Spec, 25

	
	Prove: xn => ALL(y):[yn => EXIST(z):[zn & (x,y,z)add]]
	
	Suppose...

	27	xn
		Premise

	Sufficient:  For ALL(y):[yn => EXIST(z):[dn & (x,y,z)add]]
	
	Apply the Induction shortcut (on Numbers menu).

	28	EXIST(z):[zn & (x,1,z)add] 
		& ALL(y):[yn & EXIST(z):[zn & (x,y,z)add] 
		=> EXIST(z):[zn & (x,next(y),z)add]] 
		=> ALL(y):[yn => EXIST(z):[zn & (x,y,z)add]]
		Induction

	Prove: (x,1,next(x))add  (the case for y=1)
	
	Applying the definition add...

	29	ALL(b):ALL(c):[(x,b,c)add 
		<=> (x,b,c)n3 & [b=1 & next(x)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=b & next(c')=c]]]
		U Spec, 21

	30	ALL(c):[(x,1,c)add 
		<=> (x,1,c)n3 & [1=1 & next(x)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=c]]]
		U Spec, 29

	31	(x,1,next(x))add 
		<=> (x,1,next(x))n3 & [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]]
		U Spec, 30

	32	[(x,1,next(x))add => (x,1,next(x))n3 & [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]]] 
		& [(x,1,next(x))n3 & [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]] => (x,1,next(x))add]
		Iff-And, 31

	33	(x,1,next(x))add => (x,1,next(x))n3 & [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]]
		Split, 32

	Sufficient: For (x,1,next(x))add

	34	(x,1,next(x))n3 & [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]] => (x,1,next(x))add
		Split, 32

	Prove: (x,1,next(x))n3
	
	Applying the definition of n3...

	35	ALL(c2):ALL(c3):[(x,c2,c3)n3 <=> xn & c2n & c3n]
		U Spec, 17

	36	ALL(c3):[(x,1,c3)n3 <=> xn & 1n & c3n]
		U Spec, 35

	37	(x,1,next(x))n3 <=> xn & 1n & next(x)n
		U Spec, 36

	38	[(x,1,next(x))n3 => xn & 1n & next(x)n] 
		& [xn & 1n & next(x)n => (x,1,next(x))n3]
		Iff-And, 37

	39	(x,1,next(x))n3 => xn & 1n & next(x)n
		Split, 38

	Sufficient: For (x,1,next(x))n3

	40	xn & 1n & next(x)n => (x,1,next(x))n3
		Split, 38

	41	xn => next(x)n
		U Spec, 4

	42	next(x)n
		Detach, 41, 27

	43	xn & 1n
		Join, 27, 3

	44	xn & 1n & next(x)n
		Join, 43, 42

	As Required:

	45	(x,1,next(x))n3
		Detach, 40, 44

	Prove: 1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]

	46	1=1
		Reflex

	47	next(x)=next(x)
		Reflex

	48	1=1 & next(x)=next(x)
		Join, 46, 47

	As Required:

	49	1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]
		Arb Or, 48

	50	(x,1,next(x))n3 
		& [1=1 & next(x)=next(x) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=1 & next(c')=next(x)]]
		Join, 45, 49

	51	(x,1,next(x))add
		Detach, 34, 50

	52	next(x)n & (x,1,next(x))add
		Join, 42, 51

	As Required: The case for y=1

	53	EXIST(z):[zn & (x,1,z)add]
		E Gen, 52

		
		Prove: yn & EXIST(z):[zn & (x,y,z)add] 
		       => EXIST(z):[zn & (x,next(y),z)add]
		
		The case for if true for y, then true for next(y)  (y+1)
		
		Suppose...

		54	yn & EXIST(z):[zn & (x,y,z)add]
			Premise

		55	yn
			Split, 54

		56	EXIST(z):[zn & (x,y,z)add]
			Split, 54

		Define: z

		57	zn & (x,y,z)add
			E Spec, 56

		58	zn
			Split, 57

		59	(x,y,z)add
			Split, 57

		Prove: (x,next(y),next(z))add
		
		Applying the definition of add...

		60	ALL(b):ALL(c):[(x,b,c)add 
			<=> (x,b,c)n3 & [b=1 & next(x)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=b & next(c')=c]]]
			U Spec, 21

		61	ALL(c):[(x,next(y),c)add 
			<=> (x,next(y),c)n3 & [next(y)=1 & next(x)=c | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=c]]]
			U Spec, 60

		62	(x,next(y),next(z))add 
			<=> (x,next(y),next(z))n3 & [next(y)=1 & next(x)=next(z) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=next(z)]]
			U Spec, 61

		63	[(x,next(y),next(z))add => (x,next(y),next(z))n3 & [next(y)=1 & next(x)=next(z) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=next(z)]]] 
			& [(x,next(y),next(z))n3 & [next(y)=1 & next(x)=next(z) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=next(z)]] => (x,next(y),next(z))add]
			Iff-And, 62

		64	(x,next(y),next(z))add => (x,next(y),next(z))n3 & [next(y)=1 & next(x)=next(z) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=next(z)]]
			Split, 63

		Sufficient: For (x,next(y),next(z))add

		65	(x,next(y),next(z))n3 & [next(y)=1 & next(x)=next(z) | EXIST(b'):EXIST(c'):[b'n & c'n & (x,b',c')add & next(b')=next(y) & next(c')=next(z)]] => (x,next(y),next(z))add
			Split, 63

		Prove: (x,next(y),next(z))n3
		
		Applying the definition of n3...

		66	ALL(c2):ALL(c3):[(x,c2,c3)n3 <=> xn & c2n & c3n]
			U Spec, 17

		67	ALL(c3):[(x,next(y),c3)n3 <=> xn & next(y)n & c3n]
			U Spec, 66

		68	(x,next(y),next(z))n3 <=> xn & next(y)n & next(z)n
			U Spec, 67

		69	[(x,next(y),next(z))n3 => xn & next(y)n & next(z)n] 
			& [xn & next(y)n & next(z)n => (x,next(y),next(z))n3]
			Iff-And, 68

		70	(x,next(y),next(z))n3 => xn & next(y)n & next(z)n
			Split, 69

		Sufficient: For (x,next(y),next(z))n3

		71	xn & next(y)n & next(z)n => (x,next(y),next(z))n3
			Split, 69

		72	yn => next(y)n
			U Spec, 4

		73	next(y)n
			Detach, 72, 55

		74	zn => next(z)n
			U Spec, 4

		75	next(z)n
			Detach, 74, 58

		76	xn & next(y)n
			Join, 27, 73

		77	xn & next(y)n & next(z)n
			Join, 76, 75

		As Required:

		78	(x,next(y),next(z))n3
			Detach, 71, 77

		Prove: EXIST(b):EXIST(c):[bn & cn & (x,b,c)add & next(b)=next(y) & next(c)=next(z)]

		79	next(y)=next(y)
			Reflex

		80	next(z)=next(z)
			Reflex

		81	yn & zn
			Join, 55, 58

		82	yn & zn & (x,y,z)add
			Join, 81, 59

		83	yn & zn & (x,y,z)add & next(y)=next(y)
			Join, 82, 79

		84	yn & zn & (x,y,z)add & next(y)=next(y) 
			& next(z)=next(z)
			Join, 83, 80

		85	EXIST(c):[yn & cn & (x,y,c)add & next(y)=next(y) 
			& next(c)=next(z)]
			E Gen, 84

		As Required:

		86	EXIST(b):EXIST(c):[bn & cn & (x,b,c)add & next(b)=next(y) 
			& next(c)=next(z)]
			E Gen, 85

		87	next(y)=1 & next(x)=next(z) | EXIST(b):EXIST(c):[bn & cn & (x,b,c)add & next(b)=next(y) 
			& next(c)=next(z)]
			Arb Or, 86

		88	(x,next(y),next(z))n3 
			& [next(y)=1 & next(x)=next(z) | EXIST(b):EXIST(c):[bn & cn & (x,b,c)add & next(b)=next(y) 
			& next(c)=next(z)]]
			Join, 78, 87

		As Required:

		89	(x,next(y),next(z))add
			Detach, 65, 88

		90	next(z)n & (x,next(y),next(z))add
			Join, 75, 89

		91	EXIST(c):[cn & (x,next(y),c)add]
			E Gen, 90

	As Required:
	
	The case for if true for y, then true for next(y)  (y+1)

	92	yn & EXIST(z):[zn & (x,y,z)add] 
		=> EXIST(c):[cn & (x,next(y),c)add]
		Conclusion, 54

	Generalizing...

	93	ALL(y):[yn & EXIST(z):[zn & (x,y,z)add] 
		=> EXIST(c):[cn & (x,next(y),c)add]]
		U Gen, 92

	94	EXIST(z):[zn & (x,1,z)add] 
		& ALL(y):[yn & EXIST(z):[zn & (x,y,z)add] 
		=> EXIST(c):[cn & (x,next(y),c)add]]
		Join, 53, 93

	By induction...

	95	ALL(y):[yn => EXIST(z):[zn & (x,y,z)add]]
		Detach, 28, 94

As Required: 

96	xn => ALL(y):[yn => EXIST(z):[zn & (x,y,z)add]]
	Conclusion, 27

97	ALL(x):[xn => ALL(y):[yn => EXIST(z):[zn & (x,y,z)add]]]
	U Gen, 96

	Prove: xn & yn => EXIST(z):[zn & (x,y,z)add]
	
	Suppose...

	98	xn & yn
		Premise

	99	xn
		Split, 98

	100	yn
		Split, 98

	101	xn => ALL(y):[yn => EXIST(z):[zn & (x,y,z)add]]
		U Spec, 97

	102	ALL(y):[yn => EXIST(z):[zn & (x,y,z)add]]
		Detach, 101, 99

	103	yn => EXIST(z):[zn & (x,y,z)add]
		U Spec, 102

	104	EXIST(z):[zn & (x,y,z)add]
		Detach, 103, 100

As Required:

105	xn & yn => EXIST(z):[zn & (x,y,z)add]
	Conclusion, 98

Generalizing...

106	ALL(y):[xn & yn => EXIST(z):[zn & (x,y,z)add]]
	U Gen, 105

As Required: 

For all natural numbers x and y, there exists a natural number z such that 
(x,y,z)add.

107	ALL(x):ALL(y):[xn & yn => EXIST(z):[zn & (x,y,z)add]]
	U Gen, 106