Are positive integer structures axiomatizable?

Question

Recall the first-order Peano axioms for structures of the form $(N;0,S,+,*)$:

1. $\neg \exists x Sx = 0$
2. $\forall x \forall y (Sx = Sy \rightarrow x=y)$
3. The axiom schema of induction (which are really an infinite set of axioms)
4. $\forall x (x+0)=x$
5. $\forall x \forall y (x+Sy)=S(x+y)$
6. $\forall x (x * 0) = 0$
7. $\forall x \forall y (x*Sy)=((x*y)+x)$

Define $1$ as $S0$, and define the relation $\leq$ as $x \leq y \iff \exists z (x + z) =y$. It can be shown that the set $P := \{x \in N | 1 \leq x\}$ is closed under $1$, $S$, $+$, and $*$. Therefore, we can form the structure $(P;1,S,+,*)$. I call any structure isomorphic to such a structure a positive integer structure. My question is, are positive integer structures first-order axiomatizable? I believe they are, and I believe these axioms suffice:

1. $\neg \exists x Sx = 1$
2. $\forall x \forall y (Sx = Sy \rightarrow x = y)$
3. The axiom schema of induction (but with $1$ in place of $0$ as the base case)
4. $\forall x (x + 1) = Sx$
5. $\forall x \forall y (x + Sy) = S(x+y)$
6. $\forall x (x * 1) = x$
7. $\forall x \forall y (x * Sy) = ((x*y)+x)$

Answer 1

An overkill, but still relevant, response: there is no essential "loss of information" when replacing a PA-model with its positive part. Precisely, the two are uniformly bi-interpretable. So the general strategy of a couple earlier answers of mine to questions of yours (1, 2) applies here to give axiomatizability, as well as sufficiency of your proposed axiom set for the job (we just have to check that it ensures that the corresponding interpreted structure satisfies PA).