Set of Non-negative Integers

For the set of non-negative Integers say Z+ the following axioms will hold -
1. 0 ∈ Z+ 
2. Z+ is close under an equivalence relation ' = ' .
3. ∀ x,y ∈  Z+  Then exactly one of the following relation will hold 
                           x > y , x < y , x = y 
4. Def Successor : ∀x ∈  Z+   , y ∈  Z+ and y > x  is the successor of x denoted by S(x) = y if and only if   ∄ b ∈  Z+      s.t    x < b < y . 
The axiom is ∀n ∈  Z+  S(n) ∈  (Z+  - {0}) and S(n) is a injection 

For predicate Logic to formulate induction we use another axiom :-
5. φ(0) =  true  and  ∀n ∈  Z+  φ(n) = true → φ(n+1) = true  
    ⇔  ∀n ∈  Z+  φ(n) = true [ Simple induction ]
    OR,
    φ(0) =  true  and  ∀n ∈  Z+  φ(0) ,φ(1), ... φ(n) =  true → φ(n+1) = true  
    ⇔  ∀n ∈  Z+  φ(n) = true [ Strong induction ]