In class was given these 7 (first-order) axioms of Peano arithmetic (the + denotes successor):
NT1 $\quad(\forall x) \neg\left(x^{+}=\overline{0}\right)$
NT2 $\quad(\forall x)(\forall y)\left(x^{+}=y^{+} \Rightarrow x=y\right)$
NT3 Schema: for every expression $P$ and variable symbol $x$
$$ P(\overline{0}) \Rightarrow\left((\forall x) P(x) \Rightarrow P\left(x^{+}\right)\right) \Rightarrow(\forall x) P(x) $$ NT4 $\quad(\forall x)(x+\overline{0}=x)$
NT5 $\quad(\forall x)(\forall y)\left(x+y^{+}=(x+y)^{+}\right)$
NT6 $\quad(\forall x)(x \cdot \overline{0}=0)$
NT7 $\quad(\forall x)(\forall y)\left(x \cdot\left(y^{+}\right)=(x \cdot y)+x\right)$
The task is to prove that these axioms are independent. I have figured out that to do this, I must take each axiom and find a model in which it does not hold - but all of the others do. For example, I (think) I have proved that NT1 does not hold for integers modulo (say) 5 and that NT7 does not hold true for the even natural numbers. I cannot think of how to prove NT4,NT5,NT6 because I have never come across a model in which this is not true.
For NT4, I thought of artificially creating a model in which $0+1=0$; but then NT5 would not hold because $ (0+1)^{+}=0^{+}=1 ; \quad 0+1^{+}=0+2=2 $. I also thought of trying a model ${0,1,2,...,n}$ in which $0+n = n+1$ for all $n$, but of course this would violate NT2.
Any help would be greatly appreciated :)