Constructing the Add Function

Starting with only Peano's Axioms, construct the add function. 

Prove: 

EXIST(add):[ALL(a):ALL(b):[a ε n & b ε n => add(a,b) ε n]  (i.e. add is function of 2 variables)
& 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))]


First order Peano 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 Axiom...

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

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

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