Add is Cancelable: a+b=c+b => a=c

To prove: For all numbers, a, b, c
  a+b=c+b => a=c

By Mark Hurd

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

(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

Note that this axiom is the b=1 case already.
(And is the esential step in the b=r case too.)

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

	To prove: if p, q numbers then for all b, where b is a number, p+b=q+b => p=q

	12	pn & qn
		Premise

	13	pn
		Split, 12

	14	qn
		Split, 12

	Prove: ALL(b):[bn => [p+b=q+b => p=q]]
	
	Using mathematical induction...

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

	Case: b=1

	16	ALL(b):[pn & bn & next(p)=next(b) => p=b]
		U Spec, 7

	17	pn & qn & next(p)=next(q) => p=q
		U Spec, 16

	18	pn => p+1=next(p)
		U Spec, 10

	19	qn => q+1=next(q)
		U Spec, 10

	20	p+1=next(p)
		Detach, 18, 13

	21	q+1=next(q)
		Detach, 19, 14

		22	p+1=q+1
			Premise

		23	next(p)=q+1
			Substitute, 20, 22

		24	next(p)=next(q)
			Substitute, 21, 23

		25	pn & qn & next(p)=next(q)
			Join, 12, 24

		26	p=q
			Detach, 17, 25

	Case: b=1 (done)

	27	p+1=q+1 => p=q
		Conclusion, 22

		Case: b=r

		28	rn & [p+r=q+r => p=q]
			Premise

		29	rn
			Split, 28

		30	p+r=q+r => p=q
			Split, 28

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

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

		33	pn & rn => p+next(r)=next(p+r)
			U Spec, 31

		34	qn & rn => q+next(r)=next(q+r)
			U Spec, 32

		35	pn & rn
			Join, 13, 29

		36	qn & rn
			Join, 14, 29

		37	p+next(r)=next(p+r)
			Detach, 33, 35

		38	q+next(r)=next(q+r)
			Detach, 34, 36

			39	p+next(r)=q+next(r)
				Premise

			40	next(p+r)=q+next(r)
				Substitute, 37, 39

			41	next(p+r)=next(q+r)
				Substitute, 38, 40

			42	ALL(b):[p+rn & bn & next(p+r)=next(b) => p+r=b]
				U Spec, 7

			43	p+rn & q+rn & next(p+r)=next(q+r) => p+r=q+r
				U Spec, 42

			44	ALL(b):[pn & bn => p+bn]
				U Spec, 9

			45	ALL(b):[qn & bn => q+bn]
				U Spec, 9

			46	pn & rn => p+rn
				U Spec, 44

			47	qn & rn => q+rn
				U Spec, 45

			48	p+rn
				Detach, 46, 35

			49	q+rn
				Detach, 47, 36

			50	p+rn & q+rn
				Join, 48, 49

			51	p+rn & q+rn & next(p+r)=next(q+r)
				Join, 50, 41

			52	p+r=q+r
				Detach, 43, 51

			53	p=q
				Detach, 30, 52

		54	p+next(r)=q+next(r) => p=q
			Conclusion, 39

	Case: b=r (done)

	55	rn & [p+r=q+r => p=q] => [p+next(r)=q+next(r) => p=q]
		Conclusion, 28

	56	ALL(b):[bn & [p+b=q+b => p=q] => [p+next(b)=q+next(b) => p=q]]
		U Gen, 55

	57	[p+1=q+1 => p=q]
		& ALL(b):[bn & [p+b=q+b => p=q] => [p+next(b)=q+next(b) => p=q]]
		Join, 27, 56

	Induction complete.

	58	ALL(b):[bn => [p+b=q+b => p=q]]
		Detach, 15, 57

59	pn & qn => ALL(b):[bn => [p+b=q+b => p=q]]
	Conclusion, 12

	60	pn & rn & qn
		Premise

	61	pn
		Split, 60

	62	rn
		Split, 60

	63	qn
		Split, 60

	64	pn & qn
		Join, 61, 63

	65	ALL(b):[bn => [p+b=q+b => p=q]]
		Detach, 59, 64

	66	rn => [p+r=q+r => p=q]
		U Spec, 65

	67	p+r=q+r => p=q
		Detach, 66, 62

Restated:

68	pn & rn & qn => [p+r=q+r => p=q]
	Conclusion, 60

Generalising...

69	ALL(c):[pn & rn & cn => [p+r=c+r => p=c]]
	U Gen, 68

70	ALL(b):ALL(c):[pn & bn & cn => [p+b=c+b => p=c]]
	U Gen, 69

As Required:

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