The Principal of Mathematical Induction derived from the Field Axioms

From the field axioms for the real numbers we construct the set of natural 
numbers and derive all but one of Peano's axioms, namely that no natural 
number has a successor of 1. We prove that the natural numbers, as constructed
here, uniquely satisfy the remaining axioms.

We begin by constructing the subset n of the reals such that:

Set(n)
& ALL(a):[a ε n <=> a ε real 
& ALL(b):[Set(b) & ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> a ε b]]


We prove:

1. ALL(a):[a ε n => a ε real]        (Lines 23 to 31)

   We suppose that x ε n. Applying the definition of n for x, we immediately obtain obtain x ε real.
   Then generalize on x.  

2. 1εn                               (Lines 32 to 43)

   Applying the definition of n for 1, we obtain the sufficient conditions for 1 ε n. 
   Required result then follows trivially. 

3. ALL(a):[a ε n => a+1 ε n]         (Lines 44 to 74)

   Suppose x ε n. Applying the definition of n for a=x and a=x+1, the result follows
   trivially. 

4. ALL(a):[Set(a)                    (Lines 75 to 93)
   & ALL(c):[c ε a => c ε real]
   & 1 ε a
   & ALL(c):[c ε a => c+1 ε a]
   => ALL(b):[b ε n => b ε a]]

   Suppose the antecedent is true for some set s. Then suppose the x ε n. Applying the definition
   of n for x, can easily show that x ε s. Generalize to obtain the required result. 
        
5. EXIST(nat):[Set(nat) & ALL(a):[a ε nat => a ε real] & 1 ε nat  (Lines 94 to 98)
   & ALL(a):[a ε nat => a+1 ε nat]
   & ALL(a):[Set(a)
   & ALL(c):[c ε a => c ε real]
   & 1 ε a
   & ALL(c):[c ε a => c+1 ε a]
   => ALL(b):[b ε nat => b ε a]]]

   Combine previous results and generalize.


5. P(1)                               (Lines 99 to 162)
   & ALL(a):[a ε n & P(a) => P(a+1)]
   => ALL(a):[a ε n => P(a)]

   Begin by supposing the antecedent. Then construct subset p of n such that: 
   
   ALL(a):[a ε p <=> a ε n & P(a)] 
   
   Then apply the principle of mathematical induction (for the reals) from previous result (4) for
   set p.

   That set p is a subset of the reals, follows from the previous result (1).
 
   1εp follows trivially from the definition of p.

   Suppose kεp. Applying the defintion of p for k and k+1, it is easy to show that k+1 ε p.
   Generalize this conclusion and the required result follows easily:

   ALL(a):[a ε n => P(a)]

6. n=n' given...                       (Lines 163 to 192)

   Set(n') & ALL(a):[a ε n' => a ε real] & 1 ε n'
   & ALL(a):[a ε n' => a+1 ε n']
   & ALL(a):[Set(a)
   & ALL(c):[c ε a => c ε real]
   & 1 ε a
   & ALL(c):[c ε a => c+1 ε a]
   => ALL(b):[b ε n' => b ε a]]

   Apply PMI in n for set n'. And apply PMI in n' for set n. Result follows trivially.


Field Axioms
************

1	Set(real)
	& ALL(a):ALL(b):[a ε real & b ε real => a+b ε real]
	& ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a+b+c=a+(b+c)]
	& ALL(a):ALL(b):[a ε real & b ε real => a+b=b+a]
	& 0 ε real
	& ALL(a):[a ε real => a+0=a]
	& ALL(a):[a ε real => _a ε real]
	& ALL(a):[a ε real => a+_a=0]
	& ALL(a):ALL(b):[a ε real & b ε real => a*b ε real]
	& ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a*b*c=a*(b*c)]
	& ALL(a):ALL(b):[a ε real & b ε real => a*b=b*a]
	& ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a*(b+c)=a*b+a*c]
	& 1 ε real
	& ~0=1
	& ALL(a):[a ε real => a*1=a]
	& ALL(a):[a ε real & ~a=0 => 1/a ε real]
	& ALL(a):[a ε real => a*(1/a)=1]
	Premise

Splitting into individual axioms...


Define: real, the set of real numbers

2	Set(real)
	Split, 1

Define: + operator

3	ALL(a):ALL(b):[a ε real & b ε real => a+b ε real]
	Split, 1

+ is associative

4	ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a+b+c=a+(b+c)]
	Split, 1

+ is commutative

5	ALL(a):ALL(b):[a ε real & b ε real => a+b=b+a]
	Split, 1

Define: 0

6	0 ε real
	Split, 1

7	ALL(a):[a ε real => a+0=a]
	Split, 1

Define: _x (additive invervse)

8	ALL(a):[a ε real => _a ε real]
	Split, 1

9	ALL(a):[a ε real => a+_a=0]
	Split, 1

Define: * operator

10	ALL(a):ALL(b):[a ε real & b ε real => a*b ε real]
	Split, 1

* is associative

11	ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a*b*c=a*(b*c)]
	Split, 1

* is commutative

12	ALL(a):ALL(b):[a ε real & b ε real => a*b=b*a]
	Split, 1

* is distributive over +

13	ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a*(b+c)=a*b+a*c]
	Split, 1

Define: 1

14	1 ε real
	Split, 1

15	~0=1
	Split, 1

16	ALL(a):[a ε real => a*1=a]
	Split, 1

Define: 1/x (multiplicative inverse)

17	ALL(a):[a ε real & ~a=0 => 1/a ε real]
	Split, 1

18	ALL(a):[a ε real => a*(1/a)=1]
	Split, 1

Construct n

Applying the subset axiom...

19	EXIST(n):[Set(n) & ALL(a):[a ε n <=> a ε real & ALL(b):[Set(b)
	& ALL(c):[c ε b => c ε real]
	& 1 ε b
	& ALL(c):[c ε b => c+1 ε b]
	=> a ε b]]]
	Subset, 2

Define: n, the set of natural numbers

20	Set(n) & ALL(a):[a ε n <=> a ε real & ALL(b):[Set(b)
	& ALL(c):[c ε b => c ε real]
	& 1 ε b
	& ALL(c):[c ε b => c+1 ε b]
	=> a ε b]]
	E Spec, 19

21	Set(n)
	Split, 20

22	ALL(a):[a ε n <=> a ε real & ALL(b):[Set(b)
	& ALL(c):[c ε b => c ε real]
	& 1 ε b
	& ALL(c):[c ε b => c+1 ε b]
	=> a ε b]]
	Split, 20

	Prove: x ε n => x ε real
	
	Suppose...

	23	x ε n
		Premise

	Apply definition of n for x

	24	x ε n <=> x ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x ε b]
		U Spec, 22

	25	[x ε n => x ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x ε b]]
		& [x ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x ε b] => x ε n]
		Iff-And, 24

	26	x ε n => x ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x ε b]
		Split, 25

	27	x ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x ε b] => x ε n
		Split, 25

	28	x ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x ε b]
		Detach, 26, 23

	29	x ε real
		Split, 28

As Required:

30	x ε n => x ε real
	Conclusion, 23

As Required:

31	ALL(a):[a ε n => a ε real]
	U Gen, 30

Prove: 1 ε n  

Apply defintion of n for 1

32	1 ε n <=> 1 ε real & ALL(b):[Set(b)
	& ALL(c):[c ε b => c ε real]
	& 1 ε b
	& ALL(c):[c ε b => c+1 ε b]
	=> 1 ε b]
	U Spec, 22

33	[1 ε n => 1 ε real & ALL(b):[Set(b)
	& ALL(c):[c ε b => c ε real]
	& 1 ε b
	& ALL(c):[c ε b => c+1 ε b]
	=> 1 ε b]]
	& [1 ε real & ALL(b):[Set(b)
	& ALL(c):[c ε b => c ε real]
	& 1 ε b
	& ALL(c):[c ε b => c+1 ε b]
	=> 1 ε b] => 1 ε n]
	Iff-And, 32

34	1 ε n => 1 ε real & ALL(b):[Set(b)
	& ALL(c):[c ε b => c ε real]
	& 1 ε b
	& ALL(c):[c ε b => c+1 ε b]
	=> 1 ε b]
	Split, 33

Sufficient: For 1εn

35	1 ε real & ALL(b):[Set(b)
	& ALL(c):[c ε b => c ε real]
	& 1 ε b
	& ALL(c):[c ε b => c+1 ε b]
	=> 1 ε b] => 1 ε n
	Split, 33

	Prove: Set(s)
	       & ALL(c):[c ε s => c ε real]
	       & 1 ε s
	       & ALL(c):[c ε s => c+1 ε s]
	       => 1 ε s
	
	Suppose...

	36	Set(s)
		& ALL(c):[c ε s => c ε real]
		& 1 ε s
		& ALL(c):[c ε s => c+1 ε s]
		Premise

	37	Set(s)
		Split, 36

	38	ALL(c):[c ε s => c ε real]
		Split, 36

	39	1 ε s
		Split, 36

As Required:

40	Set(s)
	& ALL(c):[c ε s => c ε real]
	& 1 ε s
	& ALL(c):[c ε s => c+1 ε s]
	=> 1 ε s
	Conclusion, 36

Generalizing...

41	ALL(b):[Set(b)
	& ALL(c):[c ε b => c ε real]
	& 1 ε b
	& ALL(c):[c ε b => c+1 ε b]
	=> 1 ε b]
	U Gen, 40

42	1 ε real
	& ALL(b):[Set(b)
	& ALL(c):[c ε b => c ε real]
	& 1 ε b
	& ALL(c):[c ε b => c+1 ε b]
	=> 1 ε b]
	Join, 14, 41

As Required:

43	1 ε n
	Detach, 35, 42

	Prove: xεn => x+1εn
	
	Suppose...

	44	x ε n
		Premise

	Apply definition of n for x

	45	x ε n <=> x ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x ε b]
		U Spec, 22

	46	[x ε n => x ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x ε b]]
		& [x ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x ε b] => x ε n]
		Iff-And, 45

	47	x ε n => x ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x ε b]
		Split, 46

	48	x ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x ε b] => x ε n
		Split, 46

	49	x ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x ε b]
		Detach, 47, 44

	50	x ε real
		Split, 49

	51	ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x ε b]
		Split, 49

	Apply definition of n for x+1

	52	x+1 ε n <=> x+1 ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x+1 ε b]
		U Spec, 22

	53	[x+1 ε n => x+1 ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x+1 ε b]]
		& [x+1 ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x+1 ε b] => x+1 ε n]
		Iff-And, 52

	54	x+1 ε n => x+1 ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x+1 ε b]
		Split, 53

	Sufficient: For x+1 ε n

	55	x+1 ε real & ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x+1 ε b] => x+1 ε n
		Split, 53

	Apply defintion of + for x and 1

	56	ALL(b):[x ε real & b ε real => x+b ε real]
		U Spec, 3

	57	x ε real & 1 ε real => x+1 ε real
		U Spec, 56

	58	x ε real & 1 ε real
		Join, 50, 14

	59	x+1 ε real
		Detach, 57, 58

		Prove: Set(s)
		       & ALL(c):[c ε s => c ε real]
		       & 1 ε s
		       & ALL(c):[c ε s => c+1 ε s]
		       => x+1 ε s
		
		Suppose...

		60	Set(s)
			& ALL(c):[c ε s => c ε real]
			& 1 ε s
			& ALL(c):[c ε s => c+1 ε s]
			Premise

		61	Set(s)
			Split, 60

		62	ALL(c):[c ε s => c ε real]
			Split, 60

		63	1 ε s
			Split, 60

		64	ALL(c):[c ε s => c+1 ε s]
			Split, 60

		Apply PMI

		65	Set(s)
			& ALL(c):[c ε s => c ε real]
			& 1 ε s
			& ALL(c):[c ε s => c+1 ε s]
			=> x ε s
			U Spec, 51

		66	x ε s
			Detach, 65, 60

		Apply defintion of s

		67	x ε s => x+1 ε s
			U Spec, 64

		68	x+1 ε s
			Detach, 67, 66

	As Required:

	69	Set(s)
		& ALL(c):[c ε s => c ε real]
		& 1 ε s
		& ALL(c):[c ε s => c+1 ε s]
		=> x+1 ε s
		Conclusion, 60

	Generalizing...

	70	ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x+1 ε b]
		U Gen, 69

	71	x+1 ε real
		& ALL(b):[Set(b)
		& ALL(c):[c ε b => c ε real]
		& 1 ε b
		& ALL(c):[c ε b => c+1 ε b]
		=> x+1 ε b]
		Join, 59, 70

	72	x+1 ε n
		Detach, 55, 71

As Required:

73	x ε n => x+1 ε n
	Conclusion, 44

As Required:

74	ALL(a):[a ε n => a+1 ε n]
	U Gen, 73

	Prove: Set(s)
	       & ALL(c):[c ε s => c ε real]
	       & 1 ε s
	       & ALL(c):[c ε s => c+1 ε s]
	       => ALL(b):[b ε n => b ε s]
	
	Suppose...

	75	Set(s)
		& ALL(c):[c ε s => c ε real]
		& 1 ε s
		& ALL(c):[c ε s => c+1 ε s]
		Premise

	76	Set(s)
		Split, 75

	77	ALL(c):[c ε s => c ε real]
		Split, 75

	78	1 ε s
		Split, 75

	79	ALL(c):[c ε s => c+1 ε s]
		Split, 75

		Prove: xεn => xεs

		80	x ε n
			Premise

		Apply definition of n for x

		81	x ε n <=> x ε real & ALL(b):[Set(b)
			& ALL(c):[c ε b => c ε real]
			& 1 ε b
			& ALL(c):[c ε b => c+1 ε b]
			=> x ε b]
			U Spec, 22

		82	[x ε n => x ε real & ALL(b):[Set(b)
			& ALL(c):[c ε b => c ε real]
			& 1 ε b
			& ALL(c):[c ε b => c+1 ε b]
			=> x ε b]]
			& [x ε real & ALL(b):[Set(b)
			& ALL(c):[c ε b => c ε real]
			& 1 ε b
			& ALL(c):[c ε b => c+1 ε b]
			=> x ε b] => x ε n]
			Iff-And, 81

		83	x ε n => x ε real & ALL(b):[Set(b)
			& ALL(c):[c ε b => c ε real]
			& 1 ε b
			& ALL(c):[c ε b => c+1 ε b]
			=> x ε b]
			Split, 82

		84	x ε real & ALL(b):[Set(b)
			& ALL(c):[c ε b => c ε real]
			& 1 ε b
			& ALL(c):[c ε b => c+1 ε b]
			=> x ε b] => x ε n
			Split, 82

		85	x ε real & ALL(b):[Set(b)
			& ALL(c):[c ε b => c ε real]
			& 1 ε b
			& ALL(c):[c ε b => c+1 ε b]
			=> x ε b]
			Detach, 83, 80

		86	x ε real
			Split, 85

		87	ALL(b):[Set(b)
			& ALL(c):[c ε b => c ε real]
			& 1 ε b
			& ALL(c):[c ε b => c+1 ε b]
			=> x ε b]
			Split, 85

		88	Set(s)
			& ALL(c):[c ε s => c ε real]
			& 1 ε s
			& ALL(c):[c ε s => c+1 ε s]
			=> x ε s
			U Spec, 87

		89	x ε s
			Detach, 88, 75

	As Required:

	90	x ε n => x ε s
		Conclusion, 80

	91	ALL(b):[b ε n => b ε s]
		U Gen, 90

As Required:

92	Set(s)
	& ALL(c):[c ε s => c ε real]
	& 1 ε s
	& ALL(c):[c ε s => c+1 ε s]
	=> ALL(b):[b ε n => b ε s]
	Conclusion, 75

As Required:

93	ALL(a):[Set(a)
	& ALL(c):[c ε a => c ε real]
	& 1 ε a
	& ALL(c):[c ε a => c+1 ε a]
	=> ALL(b):[b ε n => b ε a]]
	U Gen, 92

94	Set(n) & ALL(a):[a ε n => a ε real]
	Join, 21, 31

95	Set(n) & ALL(a):[a ε n => a ε real] & 1 ε n
	Join, 94, 43

96	Set(n) & ALL(a):[a ε n => a ε real] & 1 ε n
	& ALL(a):[a ε n => a+1 ε n]
	Join, 95, 74

97	Set(n) & ALL(a):[a ε n => a ε real] & 1 ε n
	& ALL(a):[a ε n => a+1 ε n]
	& ALL(a):[Set(a)
	& ALL(c):[c ε a => c ε real]
	& 1 ε a
	& ALL(c):[c ε a => c+1 ε a]
	=> ALL(b):[b ε n => b ε a]]
	Join, 96, 93

98	EXIST(nat):[Set(nat) & ALL(a):[a ε nat => a ε real] & 1 ε nat
	& ALL(a):[a ε nat => a+1 ε nat]
	& ALL(a):[Set(a)
	& ALL(c):[c ε a => c ε real]
	& 1 ε a
	& ALL(c):[c ε a => c+1 ε a]
	=> ALL(b):[b ε nat => b ε a]]]
	E Gen, 97

	Prove: P(1)
	       & ALL(a):[a ε n & P(a) => P(a+1)]
	       => ALL(a):[a ε n => P(a)]
	
	Suppose...

	99	P(1)
		& ALL(a):[a ε n & P(a) => P(a+1)]
		Premise

	100	P(1)
		Split, 99

	101	ALL(a):[a ε n & P(a) => P(a+1)]
		Split, 99

	Apply subset axiom

	102	EXIST(p):[Set(p) & ALL(a):[a ε p <=> a ε n & P(a)]]
		Subset, 21

	Define: p, those natural x numbers for which P(x) is true

	103	Set(p) & ALL(a):[a ε p <=> a ε n & P(a)]
		E Spec, 102

	104	Set(p)
		Split, 103

	105	ALL(a):[a ε p <=> a ε n & P(a)]
		Split, 103

	Sufficient: For ALL(b):[b ε n => b ε p]
	
	Apply PMI

	106	Set(p)
		& ALL(c):[c ε p => c ε real]
		& 1 ε p
		& ALL(c):[c ε p => c+1 ε p]
		=> ALL(b):[b ε n => b ε p]
		U Spec, 93

	107	1 ε p <=> 1 ε n & P(1)
		U Spec, 105

	108	[1 ε p => 1 ε n & P(1)] & [1 ε n & P(1) => 1 ε p]
		Iff-And, 107

	109	1 ε p => 1 ε n & P(1)
		Split, 108

	110	1 ε n & P(1) => 1 ε p
		Split, 108

	111	1 ε n & P(1)
		Join, 43, 100

	As Required:

	112	1 ε p
		Detach, 110, 111

		Prove: kεp => k+1εp
		
		Suppose...

		113	k ε p
			Premise

		Apply definition of p for k

		114	k ε p <=> k ε n & P(k)
			U Spec, 105

		115	[k ε p => k ε n & P(k)] & [k ε n & P(k) => k ε p]
			Iff-And, 114

		116	k ε p => k ε n & P(k)
			Split, 115

		117	k ε n & P(k) => k ε p
			Split, 115

		118	k ε n & P(k)
			Detach, 116, 113

		119	k ε n
			Split, 118

		120	P(k)
			Split, 118

		Apply definition of p for k+1

		121	k+1 ε p <=> k+1 ε n & P(k+1)
			U Spec, 105

		122	[k+1 ε p => k+1 ε n & P(k+1)]
			& [k+1 ε n & P(k+1) => k+1 ε p]
			Iff-And, 121

		123	k+1 ε p => k+1 ε n & P(k+1)
			Split, 122

		Sufficient: For k+1 ε p

		124	k+1 ε n & P(k+1) => k+1 ε p
			Split, 122

		Apply previous result.

		125	k ε n => k+1 ε n
			U Spec, 74

		126	k+1 ε n
			Detach, 125, 119

		Apply premise

		127	k ε n & P(k) => P(k+1)
			U Spec, 101

		128	k ε n & P(k)
			Join, 119, 120

		129	P(k+1)
			Detach, 127, 128

		130	k+1 ε n & P(k+1)
			Join, 126, 129

		131	k+1 ε p
			Detach, 124, 130

	As Required:

	132	k ε p => k+1 ε p
		Conclusion, 113

	As Required:

	133	ALL(c):[c ε p => c+1 ε p]
		U Gen, 132

		Prove: k ε p => k ε real
		
		Suppose...

		134	k ε p
			Premise

		Apply definition of p

		135	k ε p <=> k ε n & P(k)
			U Spec, 105

		136	[k ε p => k ε n & P(k)] & [k ε n & P(k) => k ε p]
			Iff-And, 135

		137	k ε p => k ε n & P(k)
			Split, 136

		138	k ε n & P(k) => k ε p
			Split, 136

		139	k ε n & P(k)
			Detach, 137, 134

		140	k ε n
			Split, 139

		141	P(k)
			Split, 139

		Apply previous result

		142	k ε n => k ε real
			U Spec, 31

		143	k ε real
			Detach, 142, 140

	As Required:

	144	k ε p => k ε real
		Conclusion, 134

	As Required:

	145	ALL(c):[c ε p => c ε real]
		U Gen, 144

	146	Set(p) & ALL(c):[c ε p => c ε real]
		Join, 104, 145

	147	Set(p) & ALL(c):[c ε p => c ε real] & 1 ε p
		Join, 146, 112

	148	Set(p) & ALL(c):[c ε p => c ε real] & 1 ε p
		& ALL(c):[c ε p => c+1 ε p]
		Join, 147, 133

	As Required:

	149	ALL(b):[b ε n => b ε p]
		Detach, 106, 148

		Prove: k ε n => P(k)
		
		Suppose...

		150	k ε n
			Premise

		151	k ε n => k ε p
			U Spec, 149

		152	k ε p
			Detach, 151, 150

		153	k ε p <=> k ε n & P(k)
			U Spec, 105

		154	[k ε p => k ε n & P(k)] & [k ε n & P(k) => k ε p]
			Iff-And, 153

		155	k ε p => k ε n & P(k)
			Split, 154

		156	k ε n & P(k) => k ε p
			Split, 154

		157	k ε n & P(k)
			Detach, 155, 152

		158	k ε n
			Split, 157

		159	P(k)
			Split, 157

	As Required:

	160	k ε n => P(k)
		Conclusion, 150

	Generalizing...

	161	ALL(a):[a ε n => P(a)]
		U Gen, 160

As Required:

162	P(1)
	& ALL(a):[a ε n & P(a) => P(a+1)]
	=> ALL(a):[a ε n => P(a)]
	Conclusion, 99

Prove: n=n' given...

163	Set(n') & ALL(a):[a ε n' => a ε real] & 1 ε n'
	& ALL(a):[a ε n' => a+1 ε n']
	& ALL(a):[Set(a)
	& ALL(c):[c ε a => c ε real]
	& 1 ε a
	& ALL(c):[c ε a => c+1 ε a]
	=> ALL(b):[b ε n' => b ε a]]
	E Spec, 98

164	Set(n')
	Split, 163

165	ALL(a):[a ε n' => a ε real]
	Split, 163

166	1 ε n'
	Split, 163

167	ALL(a):[a ε n' => a+1 ε n']
	Split, 163

168	ALL(a):[Set(a)
	& ALL(c):[c ε a => c ε real]
	& 1 ε a
	& ALL(c):[c ε a => c+1 ε a]
	=> ALL(b):[b ε n' => b ε a]]
	Split, 163

169	ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c ε a <=> c ε b]]]
	Set Equality

170	ALL(b):[Set(n) & Set(b) => [n=b <=> ALL(c):[c ε n <=> c ε b]]]
	U Spec, 169

171	Set(n) & Set(n') => [n=n' <=> ALL(c):[c ε n <=> c ε n']]
	U Spec, 170

172	Set(n) & Set(n')
	Join, 21, 164

173	n=n' <=> ALL(c):[c ε n <=> c ε n']
	Detach, 171, 172

174	[n=n' => ALL(c):[c ε n <=> c ε n']]
	& [ALL(c):[c ε n <=> c ε n'] => n=n']
	Iff-And, 173

175	n=n' => ALL(c):[c ε n <=> c ε n']
	Split, 174

Sufficient: For n=n'

176	ALL(c):[c ε n <=> c ε n'] => n=n'
	Split, 174

Apply PMI in n

177	Set(n')
	& ALL(c):[c ε n' => c ε real]
	& 1 ε n'
	& ALL(c):[c ε n' => c+1 ε n']
	=> ALL(b):[b ε n => b ε n']
	U Spec, 93

178	Set(n') & ALL(a):[a ε n' => a ε real]
	Join, 164, 165

179	Set(n') & ALL(a):[a ε n' => a ε real] & 1 ε n'
	Join, 178, 166

180	Set(n') & ALL(a):[a ε n' => a ε real] & 1 ε n'
	& ALL(a):[a ε n' => a+1 ε n']
	Join, 179, 167

181	ALL(b):[b ε n => b ε n']
	Detach, 177, 180

Apply PMI in n'

182	Set(n)
	& ALL(c):[c ε n => c ε real]
	& 1 ε n
	& ALL(c):[c ε n => c+1 ε n]
	=> ALL(b):[b ε n' => b ε n]
	U Spec, 168

183	Set(n) & ALL(a):[a ε n => a ε real]
	Join, 21, 31

184	Set(n) & ALL(a):[a ε n => a ε real] & 1 ε n
	Join, 183, 43

185	Set(n) & ALL(a):[a ε n => a ε real] & 1 ε n
	& ALL(a):[a ε n => a+1 ε n]
	Join, 184, 74

186	ALL(b):[b ε n' => b ε n]
	Detach, 182, 185

187	k ε n => k ε n'
	U Spec, 181

188	k ε n' => k ε n
	U Spec, 186

189	[k ε n => k ε n'] & [k ε n' => k ε n]
	Join, 187, 188

190	k ε n <=> k ε n'
	Iff-And, 189

191	ALL(a):[a ε n <=> a ε n']
	U Gen, 190

As Required: 

The subset n uniquely satisfies the remaining Peano Axioms?????

192	n=n'
	Detach, 176, 191