Addition is Associative

Prove: + is associative on the natural numbers

(F5 to view highlights only)


Peano's Axioms

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

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 + on 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

	
	Prove: xn => ALL(y):[yn => ALL(z):[zn => x+y+z=x+(y+z)]]
	
	Suppose...

	12	xn
		Premise

		
		Prove: yn => ALL(z):[zn => x+y+z=x+(y+z)]
		
		Suppose...

		13	yn
			Premise

		Sufficient: For ALL(z):[zn => x+y+z=x+(y+z)]
		
		Applying the induction rule...

		14	x+y+1=x+(y+1)
			& ALL(z):[zn & x+y+z=x+(y+z) => x+y+next(z)=x+(y+next(z))]
			=> ALL(z):[zn => x+y+z=x+(y+z)]
			Induction

		Prove: x+y+1=x+(y+1) (the case for z=1)
		
		Applying the definition of +...

		15	ALL(b):[xn & bn => x+next(b)=next(x+b)]
			U Spec, 11

		16	xn & yn => x+next(y)=next(x+y)
			U Spec, 15

		17	xn & yn
			Join, 12, 13

		18	x+next(y)=next(x+y)
			Detach, 16, 17

		19	yn => y+1=next(y)
			U Spec, 10

		20	y+1=next(y)
			Detach, 19, 13

		21	x+(y+1)=next(x+y)
			Substitute, 20, 18

		Applying the definition of +...

		22	x+yn => x+y+1=next(x+y)
			U Spec, 10

		23	ALL(b):[xn & bn => x+bn]
			U Spec, 9

		24	xn & yn => x+yn
			U Spec, 23

		25	x+yn
			Detach, 24, 17

		26	x+y+1=next(x+y)
			Detach, 22, 25

		As Required: Case for z=1
		
		Subsituting...

		27	x+y+1=x+(y+1)
			Substitute, 21, 26

			
			Prove: zn & x+y+z=x+(y+z) => x+y+next(z)=x+(y+next(z))
			
			Suppose...

			28	zn & x+y+z=x+(y+z)
				Premise

			29	zn
				Split, 28

			30	x+y+z=x+(y+z)
				Split, 28

			Applying definition of +...

			31	ALL(b):[x+yn & bn => x+y+next(b)=next(x+y+b)]
				U Spec, 11

			32	x+yn & zn => x+y+next(z)=next(x+y+z)
				U Spec, 31

			33	ALL(b):[xn & bn => x+bn]
				U Spec, 9

			34	xn & yn => x+yn
				U Spec, 33

			35	x+yn
				Detach, 34, 17

			36	x+yn & zn
				Join, 35, 29

			37	x+y+next(z)=next(x+y+z)
				Detach, 32, 36

			Applying definition of +...

			38	x+y+zn => x+y+z+1=next(x+y+z)
				U Spec, 10

			39	ALL(b):[x+yn & bn => x+y+bn]
				U Spec, 9

			40	x+yn & zn => x+y+zn
				U Spec, 39

			41	x+y+zn
				Detach, 40, 36

			42	x+y+z+1=next(x+y+z)
				Detach, 38, 41

			43	x+y+next(z)=x+y+z+1
				Substitute, 42, 37

			44	x+(y+next(z))=x+(y+next(z))
				Reflex

			Applying definition of +...

			45	ALL(b):[yn & bn => y+next(b)=next(y+b)]
				U Spec, 11

			46	yn & zn => y+next(z)=next(y+z)
				U Spec, 45

			47	yn & zn
				Join, 13, 29

			48	y+next(z)=next(y+z)
				Detach, 46, 47

			49	x+(y+next(z))=x+next(y+z)
				Substitute, 48, 44

			Applying definition of +...

			50	ALL(b):[xn & bn => x+next(b)=next(x+b)]
				U Spec, 11

			51	xn & y+zn => x+next(y+z)=next(x+(y+z))
				U Spec, 50

			52	ALL(b):[yn & bn => y+bn]
				U Spec, 9

			53	yn & zn => y+zn
				U Spec, 52

			54	yn & zn
				Join, 13, 29

			55	y+zn
				Detach, 53, 54

			56	xn & y+zn
				Join, 12, 55

			57	x+next(y+z)=next(x+(y+z))
				Detach, 51, 56

			58	x+(y+next(z))=next(x+(y+z))
				Substitute, 57, 49

			Applying definition of +...

			59	x+(y+z)n => x+(y+z)+1=next(x+(y+z))
				U Spec, 10

			60	ALL(b):[xn & bn => x+bn]
				U Spec, 9

			61	xn & y+zn => x+(y+z)n
				U Spec, 60

			62	x+(y+z)n
				Detach, 61, 56

			63	x+(y+z)+1=next(x+(y+z))
				Detach, 59, 62

			64	x+(y+next(z))=x+(y+z)+1
				Substitute, 63, 58

			From premise, substituting...

			65	x+(y+next(z))=x+y+z+1
				Substitute, 30, 64

			66	x+y+next(z)=x+(y+next(z))
				Substitute, 65, 43

		As Required:

		67	zn & x+y+z=x+(y+z) => x+y+next(z)=x+(y+next(z))
			Conclusion, 28

		Generalizing...

		68	ALL(z):[zn & x+y+z=x+(y+z) => x+y+next(z)=x+(y+next(z))]
			U Gen, 67

		69	x+y+1=x+(y+1)
			& ALL(z):[zn & x+y+z=x+(y+z) => x+y+next(z)=x+(y+next(z))]
			Join, 27, 68

		By induction...

		70	ALL(z):[zn => x+y+z=x+(y+z)]
			Detach, 14, 69

	As Required:

	71	yn => ALL(z):[zn => x+y+z=x+(y+z)]
		Conclusion, 13

	Generalizing...

	72	ALL(y):[yn => ALL(z):[zn => x+y+z=x+(y+z)]]
		U Gen, 71

As Required:

73	xn => ALL(y):[yn => ALL(z):[zn => x+y+z=x+(y+z)]]
	Conclusion, 12

Generalizing...

74	ALL(x):[xn => ALL(y):[yn => ALL(z):[zn => x+y+z=x+(y+z)]]]
	U Gen, 73

	
	Prove: xn & yn & zn => x+y+z=x+(y+z)
	
	Suppose...

	75	xn & yn & zn
		Premise

	76	xn
		Split, 75

	77	yn
		Split, 75

	78	zn
		Split, 75

	79	xn => ALL(y):[yn => ALL(z):[zn => x+y+z=x+(y+z)]]
		U Spec, 74

	80	ALL(y):[yn => ALL(z):[zn => x+y+z=x+(y+z)]]
		Detach, 79, 76

	81	yn => ALL(z):[zn => x+y+z=x+(y+z)]
		U Spec, 80

	82	ALL(z):[zn => x+y+z=x+(y+z)]
		Detach, 81, 77

	83	zn => x+y+z=x+(y+z)
		U Spec, 82

	84	x+y+z=x+(y+z)
		Detach, 83, 78

As Required:

85	xn & yn & zn => x+y+z=x+(y+z)
	Conclusion, 75

Generalizing...

86	ALL(c):[xn & yn & cn => x+y+c=x+(y+c)]
	U Gen, 85

87	ALL(b):ALL(c):[xn & bn & cn => x+b+c=x+(b+c)]
	U Gen, 86

As Required: 

+ is associative

88	ALL(a):ALL(b):ALL(c):[an & bn & cn => a+b+c=a+(b+c)]
	U Gen, 87