Definition:
Subtraction: if .
Division: if .
Theorem:
8. , .
proof of 8: By F3 , ;
By F5 , ;
By F3 , ;
By Thm P1,.
9. s.t. ;
s.t. .
proof of 9: By F3 , is not equal to .
10. .
11. .
12. .
proof of 12: <= : By P8 , if , then ;
By P8 , if , then .
=> : Assume , if a = 0 we are done;
Otherwise , by P8 , is not equal to and we have ;
by cancellation (P2) , .
.
proof: By F5 ,
Theorem :
s.t.
1. ;
2. For every , ;
3. For every , .
iota(2) = iota(1+1) = iota(1) + iota(1) = 1 + 1;
iota(3) = iota(2+1) = iota(2) + iota(1) = iota(2) + 1;
......
In F2 ,