The Commutativiy of Addition for Natural Numbers

by Mark Hurd

Prove: ALL(a):ALL(b):[an & bn => b+a=a+b]

(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

Define: +

2	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

3	Set(n)
	Split, 1

4	1n
	Split, 1

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

6	ALL(a):[an => ~next(a)=1]
	Split, 1

7	ALL(a):ALL(b):[an & bn & next(a)=next(b) => a=b]
	Split, 1

8	ALL(a):[Set(a) & 1a & ALL(b):[bn & ba => next(b)a]
	=> ALL(b):[bn => ba]]
	Split, 1

9	ALL(a):ALL(b):[an & bn => a+bn]
	Split, 2

10	ALL(a):[an => a+1=next(a)]
	Split, 2

11	ALL(a):ALL(b):[an & bn => a+next(b)=next(a+b)]
	Split, 2

Prove: ALL(a):[an => ALL(b):[bn => b+a=a+b]]

Applying induction shortcut...

12	ALL(b):[bn => b+1=1+b]
	& ALL(a):[an & ALL(b):[bn => b+a=a+b] => ALL(b):[bn => b+next(a)=next(a)+b]]
	=> ALL(a):[an => ALL(b):[bn => b+a=a+b]]
	Induction

Prove: ALL(b):[bn => b+1=1+b]

Applying induction shortcut...

13	1+1=1+1
	& ALL(b):[bn & b+1=1+b => next(b)+1=1+next(b)]
	=> ALL(b):[bn => b+1=1+b]
	Induction

14	1+1=1+1
	Reflex

	Prove: bn & b+1=1+b => next(b)+1=1+next(b)
	
	Suppose...

	15	bn & b+1=1+b
		Premise

	16	bn
		Split, 15

	17	b+1=1+b
		Split, 15

	Applying definition of +...

	18	bn => b+1=next(b)
		U Spec, 10

	19	b+1=next(b)
		Detach, 18, 16

	20	next(b)=1+b
		Substitute, 19, 17

	21	ALL(b):[1n & bn => 1+next(b)=next(1+b)]
		U Spec, 11

	22	1n & bn => 1+next(b)=next(1+b)
		U Spec, 21

	23	1n & bn => 1+next(b)=next(next(b))
		Substitute, 20, 22

	24	next(b)n => next(b)+1=next(next(b))
		U Spec, 10

	25	1n & bn
		Join, 4, 16

	26	1+next(b)=next(next(b))
		Detach, 23, 25

	27	next(b)n => next(b)+1=1+next(b)
		Substitute, 26, 24

	28	bn => next(b)n
		U Spec, 5

	29	next(b)n
		Detach, 28, 16

	30	next(b)+1=1+next(b)
		Detach, 27, 29

As Required:

31	bn & b+1=1+b => next(b)+1=1+next(b)
	Conclusion, 15

Generalizing...

32	ALL(b):[bn & b+1=1+b => next(b)+1=1+next(b)]
	U Gen, 31

33	1+1=1+1
	& ALL(b):[bn & b+1=1+b => next(b)+1=1+next(b)]
	Join, 14, 32

As Required:

34	ALL(b):[bn => b+1=1+b]
	Detach, 13, 33

	35	pn & ALL(b):[bn => b+p=p+b]
		Premise

	36	pn
		Split, 35

	37	ALL(b):[bn => b+p=p+b]
		Split, 35

	38	1+next(p)=next(p)+1
		& ALL(b):[bn & b+next(p)=next(p)+b => next(b)+next(p)=next(p)+next(b)]
		=> ALL(b):[bn => b+next(p)=next(p)+b]
		Induction

	39	pn & p+1=1+p => next(p)+1=1+next(p)
		U Spec, 32

	40	1n => 1+p=p+1
		U Spec, 37

	41	1+p=p+1
		Detach, 40, 4

	42	p+1=1+p
		Sym, 41

	43	pn & p+1=1+p
		Join, 36, 42

	44	next(p)+1=1+next(p)
		Detach, 39, 43

	45	1+next(p)=next(p)+1
		Sym, 44

		Prove: qn & q+next(p)=next(p)+q
		       => next(q)+next(p)=next(p)+next(q)
		
		Suppose...

		46	qn & q+next(p)=next(p)+q
			Premise

		47	qn
			Split, 46

		48	q+next(p)=next(p)+q
			Split, 46

		Applying the definition of +...

		49	ALL(b):[next(p)n & bn => next(p)+next(b)=next(next(p)+b)]
			U Spec, 11

		50	next(p)n & qn => next(p)+next(q)=next(next(p)+q)
			U Spec, 49

		51	ALL(b):[next(q)n & bn => next(q)+next(b)=next(next(q)+b)]
			U Spec, 11

		52	next(q)n & pn => next(q)+next(p)=next(next(q)+p)
			U Spec, 51

		53	pn => next(p)n
			U Spec, 5

		54	qn => next(q)n
			U Spec, 5

		55	next(p)n
			Detach, 53, 36

		56	next(q)n
			Detach, 54, 47

		57	next(p)n & qn
			Join, 55, 47

		58	next(q)n & pn
			Join, 56, 36

		59	next(p)+next(q)=next(next(p)+q)
			Detach, 50, 57

		60	next(q)+next(p)=next(next(q)+p)
			Detach, 52, 58

		61	ALL(b):[qn & bn => q+next(b)=next(q+b)]
			U Spec, 11

		62	qn & pn => q+next(p)=next(q+p)
			U Spec, 61

		63	qn & pn
			Join, 47, 36

		64	q+next(p)=next(q+p)
			Detach, 62, 63

		65	next(p)+q=next(q+p)
			Substitute, 48, 64

		66	qn => q+p=p+q
			U Spec, 37

		67	q+p=p+q
			Detach, 66, 47

		68	next(p)+q=next(p+q)
			Substitute, 67, 65

		69	next(q)n => next(q)+p=p+next(q)
			U Spec, 37

		70	next(q)+p=p+next(q)
			Detach, 69, 56

		71	ALL(b):[pn & bn => p+next(b)=next(p+b)]
			U Spec, 11

		72	pn & qn => p+next(q)=next(p+q)
			U Spec, 71

		73	pn & qn
			Join, 36, 47

		74	p+next(q)=next(p+q)
			Detach, 72, 73

		75	next(q)+p=next(p+q)
			Substitute, 74, 70

		76	next(p)+next(q)=next(next(p+q))
			Substitute, 68, 59

		77	next(q)+next(p)=next(next(p+q))
			Substitute, 75, 60

		78	next(q)+next(p)=next(p)+next(q)
			Substitute, 76, 77

	As Required:

	79	qn & q+next(p)=next(p)+q
		=> next(q)+next(p)=next(p)+next(q)
		Conclusion, 46

	Generalizing...

	80	ALL(b):[bn & b+next(p)=next(p)+b
		=> next(b)+next(p)=next(p)+next(b)]
		U Gen, 79

	81	1+next(p)=next(p)+1
		& ALL(b):[bn & b+next(p)=next(p)+b
		=> next(b)+next(p)=next(p)+next(b)]
		Join, 45, 80

	82	ALL(b):[bn => b+next(p)=next(p)+b]
		Detach, 38, 81

As Required:

83	pn & ALL(b):[bn => b+p=p+b]
	=> ALL(b):[bn => b+next(p)=next(p)+b]
	Conclusion, 35

Generalizing...

84	ALL(a):[an & ALL(b):[bn => b+a=a+b]
	=> ALL(b):[bn => b+next(a)=next(a)+b]]
	U Gen, 83

85	ALL(b):[bn => b+1=1+b]
	& ALL(a):[an & ALL(b):[bn => b+a=a+b]
	=> ALL(b):[bn => b+next(a)=next(a)+b]]
	Join, 34, 84

86	ALL(a):[an => ALL(b):[bn => b+a=a+b]]
	Detach, 12, 85

	Prove: pn & qn => q+p=p+q
	
	Suppose...

	87	pn & qn
		Premise

	88	pn => ALL(b):[bn => b+p=p+b]
		U Spec, 86

	89	pn
		Split, 87

	90	qn
		Split, 87

	91	ALL(b):[bn => b+p=p+b]
		Detach, 88, 89

	92	qn => q+p=p+q
		U Spec, 91

	93	q+p=p+q
		Detach, 92, 90

As Required:

94	pn & qn => q+p=p+q
	Conclusion, 87

Generalizing...

95	ALL(b):[pn & bn => b+p=p+b]
	U Gen, 94

As Required:

96	ALL(a):ALL(b):[an & bn => b+a=a+b]
	U Gen, 95