Constructing the Add Function

Theorem: Given Peano's Axioms...

EXIST(addfns):[Set(addfns)
& ALL(add):[add ε addfns
=> ALL(a):ALL(b):[a ε n & b ε n => add(a,b) ε n]
& ALL(a):[a ε n => add(a,1)=next(a)]
& ALL(a):ALL(b):[a ε n & b ε n => add(a,next(b))=next(add(a,b))]]
& ALL(add1):ALL(add2):[add1 ε addfns & add2 ε addfns
=> ALL(a):ALL(b):[a ε n & b ε n => add1(a,b)=add2(a,b)]]]


Outline of proof:

1. Construct n3, the set of ordered triples of natural numbers.
2. Construct pn3, the power set of n3, i.e. the set of all subsets of n3.
3. Construct func, a subset selected from pn3.
4. Prove that all elements of func are functions mapping NxN --> N
5. Construct adds, a subset of func.
6. Prove that all elements of adds are functions that have the required properties of an add
   function.
7. Prove that the add function is unique.
8. Define the + operator for natural numbers.


Peano's Axioms

1	Set(n)
	& 1 ε n
	& ALL(a):[a ε n => next(a) ε n]
	& ALL(a):[a ε n => ~next(a)=1]
	& ALL(a):ALL(b):[a ε n & b ε n & next(a)=next(b) => a=b]
	& ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => next(b) ε a]
	=> ALL(b):[b ε n => b ε a]]
	Premise

Splitting...

2	Set(n)
	Split, 1

3	1 ε n
	Split, 1

4	ALL(a):[a ε n => next(a) ε n]
	Split, 1

5	ALL(a):[a ε n => ~next(a)=1]
	Split, 1

6	ALL(a):ALL(b):[a ε n & b ε n & next(a)=next(b) => a=b]
	Split, 1

7	ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => next(b) ε a]
	=> ALL(b):[b ε n => b ε a]]
	Split, 1

Construct n3, the set of ordered triples of natural numbers.

Applying 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 <=> c1 ε a1 & c2 ε a2 & c3 ε 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) ε b <=> c1 ε n & c2 ε a2 & c3 ε 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) ε b <=> c1 ε n & c2 ε n & c3 ε a3]]]
	U Spec, 9

11	Set(n) & Set(n) & Set(n) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) ε b <=> c1 ε n & c2 ε n & c3 ε 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) ε b <=> c1 ε n & c2 ε n & c3 ε n]]
	Detach, 11, 13

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

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

16	Set''(n3)
	Split, 15

17	ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) ε n3 <=> c1 ε n & c2 ε n & c3 ε n]
	Split, 15

18	ALL(a):[Set''(a) => EXIST(b):[Set(b)
	& ALL(c):[c ε b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε c => (d1,d2,d3) ε a]]]]
	Power Set

19	Set''(n3) => EXIST(b):[Set(b)
	& ALL(c):[c ε b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε c => (d1,d2,d3) ε n3]]]
	U Spec, 18

20	EXIST(b):[Set(b)
	& ALL(c):[c ε b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε c => (d1,d2,d3) ε n3]]]
	Detach, 19, 16

21	Set(pn3)
	& ALL(c):[c ε pn3 <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε c => (d1,d2,d3) ε n3]]
	E Spec, 20

Define: pn3, the power set of n3

22	Set(pn3)
	Split, 21

23	ALL(c):[c ε pn3 <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε c => (d1,d2,d3) ε n3]]
	Split, 21

24	EXIST(sub):[Set(sub) & ALL(f):[f ε sub <=> f ε pn3 & [ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):(a,b,c) ε f]
	& ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) ε f & (a,b,c2) ε f => c1=c2]]]]
	Subset, 22

25	Set(func) & ALL(f):[f ε func <=> f ε pn3 & [ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):(a,b,c) ε f]
	& ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) ε f & (a,b,c2) ε f => c1=c2]]]
	E Spec, 24

Define: func, to be shown to be the set of functions of 2 variables mapping NxN to N.

26	Set(func)
	Split, 25

27	ALL(f):[f ε func <=> f ε pn3 & [ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):(a,b,c) ε f]
	& ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) ε f & (a,b,c2) ε f => c1=c2]]]
	Split, 25

28	EXIST(sub):[Set(sub) & ALL(f):[f ε sub <=> f ε func & [ALL(a):[a ε n => (a,1,next(a)) ε f]
	& ALL(a):ALL(b):ALL(c):[(a,b,c) ε f => (a,next(b),next(c)) ε f]]]]
	Subset, 26

29	Set(adds) & ALL(f):[f ε adds <=> f ε func & [ALL(a):[a ε n => (a,1,next(a)) ε f]
	& ALL(a):ALL(b):ALL(c):[(a,b,c) ε f => (a,next(b),next(c)) ε f]]]
	E Spec, 28

Define: adds, the set of all addition-like functions in func

30	Set(adds)
	Split, 29

31	ALL(f):[f ε adds <=> f ε func & [ALL(a):[a ε n => (a,1,next(a)) ε f]
	& ALL(a):ALL(b):ALL(c):[(a,b,c) ε f => (a,next(b),next(c)) ε f]]]
	Split, 29

	
	Prove: 
	
	fn ε func
	=> ALL(c1):ALL(c2):ALL(d):[c1 ε n & c2 ε n & d ε n => [d=fn(c1,c2) <=> (c1,c2,d) ε fn]]
	& ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):[c ε n & fn(a,b)=c]]
	& ALL(a):ALL(b):[a ε n & b ε n => fn(a,b) ε n]
	
	Suppose...

	32	fn ε func
		Premise

	Apply definition of functionality

	33	ALL(f):ALL(a1):ALL(a2):ALL(b):[Set''(f)
		& Set(a1) & Set(a2) & Set(b)
		& ALL(c1):ALL(c2):[c1 ε a1 & c2 ε a2 => EXIST(d):[d ε b & (c1,c2,d) ε f]]
		& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1 ε a1 & c2 ε a2 & d1 ε b & d2 ε b & (c1,c2,d1) ε f & (c1,c2,d2) ε f => d1=d2]
		=> ALL(c1):ALL(c2):ALL(d):[c1 ε a1 & c2 ε a2 & d ε b => [d=f(c1,c2) <=> (c1,c2,d) ε f]]]
		Function

	34	ALL(a1):ALL(a2):ALL(b):[Set''(fn)
		& Set(a1) & Set(a2) & Set(b)
		& ALL(c1):ALL(c2):[c1 ε a1 & c2 ε a2 => EXIST(d):[d ε b & (c1,c2,d) ε fn]]
		& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1 ε a1 & c2 ε a2 & d1 ε b & d2 ε b & (c1,c2,d1) ε fn & (c1,c2,d2) ε fn => d1=d2]
		=> ALL(c1):ALL(c2):ALL(d):[c1 ε a1 & c2 ε a2 & d ε b => [d=fn(c1,c2) <=> (c1,c2,d) ε fn]]]
		U Spec, 33

	35	ALL(a2):ALL(b):[Set''(fn)
		& Set(n) & Set(a2) & Set(b)
		& ALL(c1):ALL(c2):[c1 ε n & c2 ε a2 => EXIST(d):[d ε b & (c1,c2,d) ε fn]]
		& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1 ε n & c2 ε a2 & d1 ε b & d2 ε b & (c1,c2,d1) ε fn & (c1,c2,d2) ε fn => d1=d2]
		=> ALL(c1):ALL(c2):ALL(d):[c1 ε n & c2 ε a2 & d ε b => [d=fn(c1,c2) <=> (c1,c2,d) ε fn]]]
		U Spec, 34

	36	ALL(b):[Set''(fn)
		& Set(n) & Set(n) & Set(b)
		& ALL(c1):ALL(c2):[c1 ε n & c2 ε n => EXIST(d):[d ε b & (c1,c2,d) ε fn]]
		& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1 ε n & c2 ε n & d1 ε b & d2 ε b & (c1,c2,d1) ε fn & (c1,c2,d2) ε fn => d1=d2]
		=> ALL(c1):ALL(c2):ALL(d):[c1 ε n & c2 ε n & d ε b => [d=fn(c1,c2) <=> (c1,c2,d) ε fn]]]
		U Spec, 35

	Sufficient: For functionality of fn

	37	Set''(fn)
		& Set(n) & Set(n) & Set(n)
		& ALL(c1):ALL(c2):[c1 ε n & c2 ε n => EXIST(d):[d ε n & (c1,c2,d) ε fn]]
		& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[c1 ε n & c2 ε n & d1 ε n & d2 ε n & (c1,c2,d1) ε fn & (c1,c2,d2) ε fn => d1=d2]
		=> ALL(c1):ALL(c2):ALL(d):[c1 ε n & c2 ε n & d ε n => [d=fn(c1,c2) <=> (c1,c2,d) ε fn]]
		U Spec, 36

	Prove: Set''(func), i.e. func is set of ordered triples
	
	Apply definition of set func

	38	fn ε func <=> fn ε pn3 & [ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):(a,b,c) ε fn]
		& ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) ε fn & (a,b,c2) ε fn => c1=c2]]
		U Spec, 27

	39	[fn ε func => fn ε pn3 & [ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):(a,b,c) ε fn]
		& ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) ε fn & (a,b,c2) ε fn => c1=c2]]]
		& [fn ε pn3 & [ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):(a,b,c) ε fn]
		& ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) ε fn & (a,b,c2) ε fn => c1=c2]] => fn ε func]
		Iff-And, 38

	40	fn ε func => fn ε pn3 & [ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):(a,b,c) ε fn]
		& ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) ε fn & (a,b,c2) ε fn => c1=c2]]
		Split, 39

	41	fn ε pn3 & [ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):(a,b,c) ε fn]
		& ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) ε fn & (a,b,c2) ε fn => c1=c2]] => fn ε func
		Split, 39

	42	fn ε pn3 & [ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):(a,b,c) ε fn]
		& ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) ε fn & (a,b,c2) ε fn => c1=c2]]
		Detach, 40, 32

	From the definition of func...

	43	fn ε pn3
		Split, 42

	44	ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):(a,b,c) ε fn]
		& ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) ε fn & (a,b,c2) ε fn => c1=c2]
		Split, 42

	45	ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):(a,b,c) ε fn]
		Split, 44

	46	ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) ε fn & (a,b,c2) ε fn => c1=c2]
		Split, 44

	Apply the definition of set pn3

	47	fn ε pn3 <=> Set''(fn) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε fn => (d1,d2,d3) ε n3]
		U Spec, 23

	48	[fn ε pn3 => Set''(fn) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε fn => (d1,d2,d3) ε n3]]
		& [Set''(fn) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε fn => (d1,d2,d3) ε n3] => fn ε pn3]
		Iff-And, 47

	49	fn ε pn3 => Set''(fn) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε fn => (d1,d2,d3) ε n3]
		Split, 48

	50	Set''(fn) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε fn => (d1,d2,d3) ε n3] => fn ε pn3
		Split, 48

	51	Set''(fn) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε fn => (d1,d2,d3) ε n3]
		Detach, 49, 43

	As Required: (Functionality Part 1)

	52	Set''(fn)
		Split, 51

	53	ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε fn => (d1,d2,d3) ε n3]
		Split, 51

		
		Prove: x ε n & y ε n => EXIST(c):[c ε n & (x,y,c) ε fn]
		
		Suppose...

		54	x ε n & y ε n
			Premise

		55	x ε n
			Split, 54

		56	y ε n
			Split, 54

		From the definition of fn...

		57	ALL(b):[x ε n & b ε n => EXIST(c):(x,b,c) ε fn]
			U Spec, 45

		58	x ε n & y ε n => EXIST(c):(x,y,c) ε fn
			U Spec, 57

		59	EXIST(c):(x,y,c) ε fn
			Detach, 58, 54

		60	(x,y,z) ε fn
			E Spec, 59

		61	ALL(d2):ALL(d3):[(x,d2,d3) ε fn => (x,d2,d3) ε n3]
			U Spec, 53

		62	ALL(d3):[(x,y,d3) ε fn => (x,y,d3) ε n3]
			U Spec, 61

		63	(x,y,z) ε fn => (x,y,z) ε n3
			U Spec, 62

		64	(x,y,z) ε n3
			Detach, 63, 60

		65	ALL(c2):ALL(c3):[(x,c2,c3) ε n3 <=> x ε n & c2 ε n & c3 ε n]
			U Spec, 17

		66	ALL(c3):[(x,y,c3) ε n3 <=> x ε n & y ε n & c3 ε n]
			U Spec, 65

		67	(x,y,z) ε n3 <=> x ε n & y ε n & z ε n
			U Spec, 66

		68	[(x,y,z) ε n3 => x ε n & y ε n & z ε n]
			& [x ε n & y ε n & z ε n => (x,y,z) ε n3]
			Iff-And, 67

		69	(x,y,z) ε n3 => x ε n & y ε n & z ε n
			Split, 68

		70	x ε n & y ε n & z ε n => (x,y,z) ε n3
			Split, 68

		71	x ε n & y ε n & z ε n
			Detach, 69, 64

		72	x ε n
			Split, 71

		73	y ε n
			Split, 71

		74	z ε n
			Split, 71

		75	z ε n & (x,y,z) ε fn
			Join, 74, 60

		76	EXIST(c):[c ε n & (x,y,c) ε fn]
			E Gen, 75

	As Required:

	77	x ε n & y ε n => EXIST(c):[c ε n & (x,y,c) ε fn]
		Conclusion, 54
	Generalizing...

	78	ALL(b):[x ε n & b ε n => EXIST(c):[c ε n & (x,b,c) ε fn]]
		U Gen, 77

	As Required: (Functionality Part 2)

	79	ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):[c ε n & (a,b,c) ε fn]]
		U Gen, 78

		
		Prove: 
		
		x ε n & y ε n & z1 ε n & z2 ε n & (x,y,z1) ε fn & (x,y,z2) ε fn
		=> z1=z2
		
		Suppose...

		80	x ε n & y ε n & z1 ε n & z2 ε n & (x,y,z1) ε fn & (x,y,z2) ε fn
			Premise

		81	x ε n
			Split, 80

		82	y ε n
			Split, 80

		83	z1 ε n
			Split, 80

		84	z2 ε n
			Split, 80

		85	(x,y,z1) ε fn
			Split, 80

		86	(x,y,z2) ε fn
			Split, 80

		87	ALL(b):ALL(c1):ALL(c2):[(x,b,c1) ε fn & (x,b,c2) ε fn => c1=c2]
			U Spec, 46

		88	ALL(c1):ALL(c2):[(x,y,c1) ε fn & (x,y,c2) ε fn => c1=c2]
			U Spec, 87

		89	ALL(c2):[(x,y,z1) ε fn & (x,y,c2) ε fn => z1=c2]
			U Spec, 88

		90	(x,y,z1) ε fn & (x,y,z2) ε fn => z1=z2
			U Spec, 89

		91	(x,y,z1) ε fn & (x,y,z2) ε fn
			Join, 85, 86

		92	z1=z2
			Detach, 90, 91

	As Required:

	93	x ε n & y ε n & z1 ε n & z2 ε n & (x,y,z1) ε fn & (x,y,z2) ε fn
		=> z1=z2
		Conclusion, 80
	Generalizing...

	94	ALL(c2):[x ε n & y ε n & z1 ε n & c2 ε n & (x,y,z1) ε fn & (x,y,c2) ε fn
		=> z1=c2]
		U Gen, 93

	95	ALL(c1):ALL(c2):[x ε n & y ε n & c1 ε n & c2 ε n & (x,y,c1) ε fn & (x,y,c2) ε fn
		=> c1=c2]
		U Gen, 94

	96	ALL(b):ALL(c1):ALL(c2):[x ε n & b ε n & c1 ε n & c2 ε n & (x,b,c1) ε fn & (x,b,c2) ε fn
		=> c1=c2]
		U Gen, 95

	As Required: (Functionality Part 3)

	97	ALL(a):ALL(b):ALL(c1):ALL(c2):[a ε n & b ε n & c1 ε n & c2 ε n & (a,b,c1) ε fn & (a,b,c2) ε fn
		=> c1=c2]
		U Gen, 96

	Combining results...

	98	Set''(fn) & Set(n)
		Join, 52, 2

	99	Set''(fn) & Set(n) & Set(n)
		Join, 98, 2

	100	Set''(fn) & Set(n) & Set(n) & Set(n)
		Join, 99, 2

	101	Set''(fn) & Set(n) & Set(n) & Set(n)
		& ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):[c ε n & (a,b,c) ε fn]]
		Join, 100, 79

	102	Set''(fn) & Set(n) & Set(n) & Set(n)
		& ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):[c ε n & (a,b,c) ε fn]]
		& ALL(a):ALL(b):ALL(c1):ALL(c2):[a ε n & b ε n & c1 ε n & c2 ε n & (a,b,c1) ε fn & (a,b,c2) ε fn
		=> c1=c2]
		Join, 101, 97

	fn is a function

	103	ALL(c1):ALL(c2):ALL(d):[c1 ε n & c2 ε n & d ε n => [d=fn(c1,c2) <=> (c1,c2,d) ε fn]]
		Detach, 37, 102

		
		Prove: xεn & yεn => fn(x,y)εn
		
		Suppose...

		104	x ε n & y ε n
			Premise

		105	ALL(b):[x ε n & b ε n => EXIST(c):[c ε n & (x,b,c) ε fn]]
			U Spec, 79

		106	x ε n & y ε n => EXIST(c):[c ε n & (x,y,c) ε fn]
			U Spec, 105

		107	EXIST(c):[c ε n & (x,y,c) ε fn]
			Detach, 106, 104

		108	z ε n & (x,y,z) ε fn
			E Spec, 107

		109	z ε n
			Split, 108

		110	(x,y,z) ε fn
			Split, 108

		111	ALL(c2):ALL(d):[x ε n & c2 ε n & d ε n => [d=fn(x,c2) <=> (x,c2,d) ε fn]]
			U Spec, 103

		112	ALL(d):[x ε n & y ε n & d ε n => [d=fn(x,y) <=> (x,y,d) ε fn]]
			U Spec, 111

		113	x ε n & y ε n & z ε n => [z=fn(x,y) <=> (x,y,z) ε fn]
			U Spec, 112

		114	x ε n & y ε n & z ε n
			Join, 104, 109

		115	z=fn(x,y) <=> (x,y,z) ε fn
			Detach, 113, 114

		116	[z=fn(x,y) => (x,y,z) ε fn]
			& [(x,y,z) ε fn => z=fn(x,y)]
			Iff-And, 115

		117	z=fn(x,y) => (x,y,z) ε fn
			Split, 116

		118	(x,y,z) ε fn => z=fn(x,y)
			Split, 116

		119	z=fn(x,y)
			Detach, 118, 110

		120	fn(x,y) ε n
			Substitute, 119, 109

	As Required:

	121	x ε n & y ε n => fn(x,y) ε n
		Conclusion, 104
	Generalizing...

	122	ALL(b):[x ε n & b ε n => fn(x,b) ε n]
		U Gen, 121

	123	ALL(a):ALL(b):[a ε n & b ε n => fn(a,b) ε n]
		U Gen, 122

		
		Prove: x ε n & y ε n => EXIST(c):[c ε n & fn(x,y)=c]
		
		Suppose...

		124	x ε n & y ε n
			Premise

		125	ALL(b):[x ε n & b ε n => fn(x,b) ε n]
			U Spec, 123

		126	x ε n & y ε n => fn(x,y) ε n
			U Spec, 125

		127	fn(x,y) ε n
			Detach, 126, 124

		128	fn(x,y)=fn(x,y)
			Reflex

		129	fn(x,y) ε n & fn(x,y)=fn(x,y)
			Join, 127, 128

		130	EXIST(c):[c ε n & fn(x,y)=c]
			E Gen, 129

	As Required:

	131	x ε n & y ε n => EXIST(c):[c ε n & fn(x,y)=c]
		Conclusion, 124
	Generalizing...

	132	ALL(b):[x ε n & b ε n => EXIST(c):[c ε n & fn(x,b)=c]]
		U Gen, 131

	133	ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):[c ε n & fn(a,b)=c]]
		U Gen, 132

	134	ALL(c1):ALL(c2):ALL(d):[c1 ε n & c2 ε n & d ε n => [d=fn(c1,c2) <=> (c1,c2,d) ε fn]]
		& ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):[c ε n & fn(a,b)=c]]
		Join, 103, 133

	135	ALL(c1):ALL(c2):ALL(d):[c1 ε n & c2 ε n & d ε n => [d=fn(c1,c2) <=> (c1,c2,d) ε fn]]
		& ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):[c ε n & fn(a,b)=c]]
		& ALL(a):ALL(b):[a ε n & b ε n => fn(a,b) ε n]
		Join, 134, 123

As Required:

136	fn ε func
	=> ALL(c1):ALL(c2):ALL(d):[c1 ε n & c2 ε n & d ε n => [d=fn(c1,c2) <=> (c1,c2,d) ε fn]]
	& ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):[c ε n & fn(a,b)=c]]
	& ALL(a):ALL(b):[a ε n & b ε n => fn(a,b) ε n]
	Conclusion, 32
Generalizing...

137	ALL(f):[f ε func
	=> ALL(c1):ALL(c2):ALL(d):[c1 ε n & c2 ε n & d ε n => [d=f(c1,c2) <=> (c1,c2,d) ε f]]
	& ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):[c ε n & f(a,b)=c]]
	& ALL(a):ALL(b):[a ε n & b ε n => f(a,b) ε n]]
	U Gen, 136

	
	Prove: 
	
	fn ε adds
	=> ALL(a):ALL(b):[a ε n & b ε n => fn(a,b) ε n]
	& ALL(a):[a ε n => fn(a,1)=next(a)]
	& ALL(a):ALL(b):[a ε n & b ε n => fn(a,next(b))=next(fn(a,b))]
	
	Suppose...

	138	fn ε adds
		Premise

	139	fn ε adds <=> fn ε func & [ALL(a):[a ε n => (a,1,next(a)) ε fn]
		& ALL(a):ALL(b):ALL(c):[(a,b,c) ε fn => (a,next(b),next(c)) ε fn]]
		U Spec, 31

	140	[fn ε adds => fn ε func & [ALL(a):[a ε n => (a,1,next(a)) ε fn]
		& ALL(a):ALL(b):ALL(c):[(a,b,c) ε fn => (a,next(b),next(c)) ε fn]]]
		& [fn ε func & [ALL(a):[a ε n => (a,1,next(a)) ε fn]
		& ALL(a):ALL(b):ALL(c):[(a,b,c) ε fn => (a,next(b),next(c)) ε fn]] => fn ε adds]
		Iff-And, 139

	141	fn ε adds => fn ε func & [ALL(a):[a ε n => (a,1,next(a)) ε fn]
		& ALL(a):ALL(b):ALL(c):[(a,b,c) ε fn => (a,next(b),next(c)) ε fn]]
		Split, 140

	142	fn ε func & [ALL(a):[a ε n => (a,1,next(a)) ε fn]
		& ALL(a):ALL(b):ALL(c):[(a,b,c) ε fn => (a,next(b),next(c)) ε fn]] => fn ε adds
		Split, 140

	143	fn ε func & [ALL(a):[a ε n => (a,1,next(a)) ε fn]
		& ALL(a):ALL(b):ALL(c):[(a,b,c) ε fn => (a,next(b),next(c)) ε fn]]
		Detach, 141, 138

	144	fn ε func
		Split, 143

	145	ALL(a):[a ε n => (a,1,next(a)) ε fn]
		& ALL(a):ALL(b):ALL(c):[(a,b,c) ε fn => (a,next(b),next(c)) ε fn]
		Split, 143

	146	ALL(a):[a ε n => (a,1,next(a)) ε fn]
		Split, 145

	147	ALL(a):ALL(b):ALL(c):[(a,b,c) ε fn => (a,next(b),next(c)) ε fn]
		Split, 145

	148	fn ε func
		=> ALL(c1):ALL(c2):ALL(d):[c1 ε n & c2 ε n & d ε n => [d=fn(c1,c2) <=> (c1,c2,d) ε fn]]
		& ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):[c ε n & fn(a,b)=c]]
		& ALL(a):ALL(b):[a ε n & b ε n => fn(a,b) ε n]
		U Spec, 137

	149	ALL(c1):ALL(c2):ALL(d):[c1 ε n & c2 ε n & d ε n => [d=fn(c1,c2) <=> (c1,c2,d) ε fn]]
		& ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):[c ε n & fn(a,b)=c]]
		& ALL(a):ALL(b):[a ε n & b ε n => fn(a,b) ε n]
		Detach, 148, 144

	150	ALL(c1):ALL(c2):ALL(d):[c1 ε n & c2 ε n & d ε n => [d=fn(c1,c2) <=> (c1,c2,d) ε fn]]
		Split, 149

	151	ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):[c ε n & fn(a,b)=c]]
		Split, 149

	152	ALL(a):ALL(b):[a ε n & b ε n => fn(a,b) ε n]
		Split, 149

		
		Prove: x ε n => fn(x,1)=next(x)
		
		Suppose...

		153	x ε n
			Premise

		154	x ε n => (x,1,next(x)) ε fn
			U Spec, 146

		155	(x,1,next(x)) ε fn
			Detach, 154, 153

		156	ALL(c2):ALL(d):[x ε n & c2 ε n & d ε n => [d=fn(x,c2) <=> (x,c2,d) ε fn]]
			U Spec, 150

		157	ALL(d):[x ε n & 1 ε n & d ε n => [d=fn(x,1) <=> (x,1,d) ε fn]]
			U Spec, 156

		158	x ε n & 1 ε n & next(x) ε n => [next(x)=fn(x,1) <=> (x,1,next(x)) ε fn]
			U Spec, 157

		159	x ε n => next(x) ε n
			U Spec, 4

		160	next(x) ε n
			Detach, 159, 153

		161	x ε n & 1 ε n
			Join, 153, 3

		162	x ε n & 1 ε n & next(x) ε n
			Join, 161, 160

		163	next(x)=fn(x,1) <=> (x,1,next(x)) ε fn
			Detach, 158, 162

		164	[next(x)=fn(x,1) => (x,1,next(x)) ε fn]
			& [(x,1,next(x)) ε fn => next(x)=fn(x,1)]
			Iff-And, 163

		165	next(x)=fn(x,1) => (x,1,next(x)) ε fn
			Split, 164

		166	(x,1,next(x)) ε fn => next(x)=fn(x,1)
			Split, 164

		167	next(x)=fn(x,1)
			Detach, 166, 155

		168	fn(x,1)=next(x)
			Sym, 167

	As Required:

	169	x ε n => fn(x,1)=next(x)
		Conclusion, 153
	Generalizing...

	170	ALL(a):[a ε n => fn(a,1)=next(a)]
		U Gen, 169

		
		Prove: x ε n & y ε n => fn(x,next(y))=next(fn(x,y))
		
		Suppose...

		171	x ε n & y ε n
			Premise

		172	x ε n
			Split, 171

		173	y ε n
			Split, 171

		174	ALL(b):[x ε n & b ε n => EXIST(c):[c ε n & fn(x,b)=c]]
			U Spec, 151

		175	x ε n & y ε n => EXIST(c):[c ε n & fn(x,y)=c]
			U Spec, 174

		176	EXIST(c):[c ε n & fn(x,y)=c]
			Detach, 175, 171

		177	z ε n & fn(x,y)=z
			E Spec, 176

		178	z ε n
			Split, 177

		179	fn(x,y)=z
			Split, 177

		180	ALL(b):ALL(c):[(x,b,c) ε fn => (x,next(b),next(c)) ε fn]
			U Spec, 147

		181	ALL(c):[(x,y,c) ε fn => (x,next(y),next(c)) ε fn]
			U Spec, 180

		182	(x,y,z) ε fn => (x,next(y),next(z)) ε fn
			U Spec, 181

		183	ALL(c2):ALL(d):[x ε n & c2 ε n & d ε n => [d=fn(x,c2) <=> (x,c2,d) ε fn]]
			U Spec, 150

		184	ALL(d):[x ε n & y ε n & d ε n => [d=fn(x,y) <=> (x,y,d) ε fn]]
			U Spec, 183

		185	x ε n & y ε n & z ε n => [z=fn(x,y) <=> (x,y,z) ε fn]
			U Spec, 184

		186	x ε n & y ε n & z ε n
			Join, 171, 178

		187	z=fn(x,y) <=> (x,y,z) ε fn
			Detach, 185, 186

		188	[z=fn(x,y) => (x,y,z) ε fn]
			& [(x,y,z) ε fn => z=fn(x,y)]
			Iff-And, 187

		189	z=fn(x,y) => (x,y,z) ε fn
			Split, 188

		190	(x,y,z) ε fn => z=fn(x,y)
			Split, 188

		191	z=fn(x,y)
			Sym, 179

		192	(x,y,z) ε fn
			Detach, 189, 191

		193	(x,next(y),next(z)) ε fn
			Detach, 182, 192

		194	ALL(c2):ALL(d):[x ε n & c2 ε n & d ε n => [d=fn(x,c2) <=> (x,c2,d) ε fn]]
			U Spec, 150

		195	ALL(d):[x ε n & next(y) ε n & d ε n => [d=fn(x,next(y)) <=> (x,next(y),d) ε fn]]
			U Spec, 194

		196	x ε n & next(y) ε n & next(z) ε n => [next(z)=fn(x,next(y)) <=> (x,next(y),next(z)) ε fn]
			U Spec, 195

		197	y ε n => next(y) ε n
			U Spec, 4

		198	next(y) ε n
			Detach, 197, 173

		199	z ε n => next(z) ε n
			U Spec, 4

		200	next(z) ε n
			Detach, 199, 178

		201	x ε n & next(y) ε n
			Join, 172, 198

		202	x ε n & next(y) ε n & next(z) ε n
			Join, 201, 200

		203	next(z)=fn(x,next(y)) <=> (x,next(y),next(z)) ε fn
			Detach, 196, 202

		204	[next(z)=fn(x,next(y)) => (x,next(y),next(z)) ε fn]
			& [(x,next(y),next(z)) ε fn => next(z)=fn(x,next(y))]
			Iff-And, 203

		205	next(z)=fn(x,next(y)) => (x,next(y),next(z)) ε fn
			Split, 204

		206	(x,next(y),next(z)) ε fn => next(z)=fn(x,next(y))
			Split, 204

		207	next(z)=fn(x,next(y))
			Detach, 206, 193

		208	fn(x,next(y))=next(z)
			Sym, 207

		209	fn(x,next(y))=next(fn(x,y))
			Substitute, 179, 208

	As Required:

	210	x ε n & y ε n => fn(x,next(y))=next(fn(x,y))
		Conclusion, 171
	Generalizing...

	211	ALL(b):[x ε n & b ε n => fn(x,next(b))=next(fn(x,b))]
		U Gen, 210

	212	ALL(a):ALL(b):[a ε n & b ε n => fn(a,next(b))=next(fn(a,b))]
		U Gen, 211

	213	ALL(a):ALL(b):[a ε n & b ε n => fn(a,b) ε n]
		& ALL(a):[a ε n => fn(a,1)=next(a)]
		Join, 152, 170

	214	ALL(a):ALL(b):[a ε n & b ε n => fn(a,b) ε n]
		& ALL(a):[a ε n => fn(a,1)=next(a)]
		& ALL(a):ALL(b):[a ε n & b ε n => fn(a,next(b))=next(fn(a,b))]
		Join, 213, 212

As Required:

215	fn ε adds
	=> ALL(a):ALL(b):[a ε n & b ε n => fn(a,b) ε n]
	& ALL(a):[a ε n => fn(a,1)=next(a)]
	& ALL(a):ALL(b):[a ε n & b ε n => fn(a,next(b))=next(fn(a,b))]
	Conclusion, 138
Generalizing...

216	ALL(add):[add ε adds
	=> ALL(a):ALL(b):[a ε n & b ε n => add(a,b) ε n]
	& ALL(a):[a ε n => add(a,1)=next(a)]
	& ALL(a):ALL(b):[a ε n & b ε n => add(a,next(b))=next(add(a,b))]]
	U Gen, 215

	
	Prove: add1 ε adds & add2 ε adds => ALL(a):ALL(b):[aεn & bεn =>  add1(a,b)=add2(a,b)]
	
	Suppose...

	217	add1 ε adds & add2 ε adds
		Premise

	218	add1 ε adds
		Split, 217

	219	add2 ε adds
		Split, 217

	220	add1 ε adds
		=> ALL(a):ALL(b):[a ε n & b ε n => add1(a,b) ε n]
		& ALL(a):[a ε n => add1(a,1)=next(a)]
		& ALL(a):ALL(b):[a ε n & b ε n => add1(a,next(b))=next(add1(a,b))]
		U Spec, 216

	221	ALL(a):ALL(b):[a ε n & b ε n => add1(a,b) ε n]
		& ALL(a):[a ε n => add1(a,1)=next(a)]
		& ALL(a):ALL(b):[a ε n & b ε n => add1(a,next(b))=next(add1(a,b))]
		Detach, 220, 218

	Properties of add1

	222	ALL(a):ALL(b):[a ε n & b ε n => add1(a,b) ε n]
		Split, 221

	223	ALL(a):[a ε n => add1(a,1)=next(a)]
		Split, 221

	224	ALL(a):ALL(b):[a ε n & b ε n => add1(a,next(b))=next(add1(a,b))]
		Split, 221

	225	add2 ε adds
		=> ALL(a):ALL(b):[a ε n & b ε n => add2(a,b) ε n]
		& ALL(a):[a ε n => add2(a,1)=next(a)]
		& ALL(a):ALL(b):[a ε n & b ε n => add2(a,next(b))=next(add2(a,b))]
		U Spec, 216

	226	ALL(a):ALL(b):[a ε n & b ε n => add2(a,b) ε n]
		& ALL(a):[a ε n => add2(a,1)=next(a)]
		& ALL(a):ALL(b):[a ε n & b ε n => add2(a,next(b))=next(add2(a,b))]
		Detach, 225, 219

	Properties of add2

	227	ALL(a):ALL(b):[a ε n & b ε n => add2(a,b) ε n]
		Split, 226

	228	ALL(a):[a ε n => add2(a,1)=next(a)]
		Split, 226

	229	ALL(a):ALL(b):[a ε n & b ε n => add2(a,next(b))=next(add2(a,b))]
		Split, 226

		
		Prove: x ε n => ALL(k):[k ε n => add1(x,k)=add2(x,k)]
		
		Suppose...

		230	x ε n
			Premise

		Using Induction Shortcut...

		231	add1(x,1)=add2(x,1)
			& ALL(k):[k ε n & add1(x,k)=add2(x,k) => add1(x,next(k))=add2(x,next(k))]
			=> ALL(k):[k ε n => add1(x,k)=add2(x,k)]
			Induction

		232	x ε n => add1(x,1)=next(x)
			U Spec, 223

		233	add1(x,1)=next(x)
			Detach, 232, 230

		234	x ε n => add2(x,1)=next(x)
			U Spec, 228

		235	add2(x,1)=next(x)
			Detach, 234, 230

		As Required: (Induction Part 1)

		236	add1(x,1)=add2(x,1)
			Substitute, 235, 233

			
			Prove: 
			
			y ε n & add1(x,y)=add2(x,y)
			=> add1(x,next(y))=add2(x,next(y))
			
			Suppose...

			237	y ε n & add1(x,y)=add2(x,y)
				Premise

			238	y ε n
				Split, 237

			239	add1(x,y)=add2(x,y)
				Split, 237

			240	ALL(b):[x ε n & b ε n => add1(x,next(b))=next(add1(x,b))]
				U Spec, 224

			241	x ε n & y ε n => add1(x,next(y))=next(add1(x,y))
				U Spec, 240

			242	x ε n & y ε n
				Join, 230, 238

			243	add1(x,next(y))=next(add1(x,y))
				Detach, 241, 242

			244	ALL(b):[x ε n & b ε n => add2(x,next(b))=next(add2(x,b))]
				U Spec, 229

			245	x ε n & y ε n => add2(x,next(y))=next(add2(x,y))
				U Spec, 244

			246	add2(x,next(y))=next(add2(x,y))
				Detach, 245, 242

			247	add2(x,next(y))=next(add1(x,y))
				Substitute, 239, 246

			248	add1(x,next(y))=add2(x,next(y))
				Substitute, 247, 243

		As Required:

		249	y ε n & add1(x,y)=add2(x,y)
			=> add1(x,next(y))=add2(x,next(y))
			Conclusion, 237
		As Required: (Induction Part 2)

		250	ALL(k):[k ε n & add1(x,k)=add2(x,k)
			=> add1(x,next(k))=add2(x,next(k))]
			U Gen, 249

		251	add1(x,1)=add2(x,1)
			& ALL(k):[k ε n & add1(x,k)=add2(x,k)
			=> add1(x,next(k))=add2(x,next(k))]
			Join, 236, 250

		By induction...

		252	ALL(k):[k ε n => add1(x,k)=add2(x,k)]
			Detach, 231, 251

	As Required:

	253	x ε n => ALL(k):[k ε n => add1(x,k)=add2(x,k)]
		Conclusion, 230
	Generalizing...

	254	ALL(a):[a ε n => ALL(k):[k ε n => add1(a,k)=add2(a,k)]]
		U Gen, 253

		
		Prove: x ε n & y ε n => add1(x,y)=add2(x,y)
		
		Suppose...

		255	x ε n & y ε n
			Premise

		256	x ε n
			Split, 255

		257	y ε n
			Split, 255

		258	x ε n => ALL(k):[k ε n => add1(x,k)=add2(x,k)]
			U Spec, 254

		259	ALL(k):[k ε n => add1(x,k)=add2(x,k)]
			Detach, 258, 256

		260	y ε n => add1(x,y)=add2(x,y)
			U Spec, 259

		261	add1(x,y)=add2(x,y)
			Detach, 260, 257

	As Required:

	262	x ε n & y ε n => add1(x,y)=add2(x,y)
		Conclusion, 255
	Generalizing...

	263	ALL(b):[x ε n & b ε n => add1(x,b)=add2(x,b)]
		U Gen, 262

	264	ALL(a):ALL(b):[a ε n & b ε n => add1(a,b)=add2(a,b)]
		U Gen, 263

As Required:

265	add1 ε adds & add2 ε adds
	=> ALL(a):ALL(b):[a ε n & b ε n => add1(a,b)=add2(a,b)]
	Conclusion, 217
266	ALL(add2):[add1 ε adds & add2 ε adds
	=> ALL(a):ALL(b):[a ε n & b ε n => add1(a,b)=add2(a,b)]]
	U Gen, 265

The add function is unique

267	ALL(add1):ALL(add2):[add1 ε adds & add2 ε adds
	=> ALL(a):ALL(b):[a ε n & b ε n => add1(a,b)=add2(a,b)]]
	U Gen, 266

Combining results...

268	Set(adds)
	& ALL(add):[add ε adds
	=> ALL(a):ALL(b):[a ε n & b ε n => add(a,b) ε n]
	& ALL(a):[a ε n => add(a,1)=next(a)]
	& ALL(a):ALL(b):[a ε n & b ε n => add(a,next(b))=next(add(a,b))]]
	Join, 30, 216

269	Set(adds)
	& ALL(add):[add ε adds
	=> ALL(a):ALL(b):[a ε n & b ε n => add(a,b) ε n]
	& ALL(a):[a ε n => add(a,1)=next(a)]
	& ALL(a):ALL(b):[a ε n & b ε n => add(a,next(b))=next(add(a,b))]]
	& ALL(add1):ALL(add2):[add1 ε adds & add2 ε adds
	=> ALL(a):ALL(b):[a ε n & b ε n => add1(a,b)=add2(a,b)]]
	Join, 268, 267

As Required:

270	EXIST(addfns):[Set(addfns)
	& ALL(add):[add ε addfns
	=> ALL(a):ALL(b):[a ε n & b ε n => add(a,b) ε n]
	& ALL(a):[a ε n => add(a,1)=next(a)]
	& ALL(a):ALL(b):[a ε n & b ε n => add(a,next(b))=next(add(a,b))]]
	& ALL(add1):ALL(add2):[add1 ε addfns & add2 ε addfns
	=> ALL(a):ALL(b):[a ε n & b ε n => add1(a,b)=add2(a,b)]]]
	E Gen, 269

This provides the rationale for the usual definition of the + operator for natural numbers:

271	ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
	& ALL(a):[a ε n => a+1=next(a)]
	& ALL(a):ALL(b):[a ε n & b ε n => a+next(b)=next(a+b)]
	Definition