Reference request: Minimal Axiomatizations of PA over (+,x,<=). Many years ago, when I was still a high school student, I came up with a certain first-order axiomatization of PA over the signature (+, x, &leq;). Out of nostalgia, I've decided to clean up what I did, and so am curious for a reference to what are known to be minimal axiomatizations of PA over that signature.
EDIT:
In particular, I am interested in axiomatizations consisting of a finite list of axioms plus an axiom schema of well-ordering such as $\exists x\phi(x)\implies\exists x\left(\left(\phi(x)\wedge \forall y(\phi(y)\implies x\leq y)\right)\right)$, and not a finite list of axioms plus an axiom schema for induction such as $\left(\phi(0)\wedge\forall x\left(\phi(x)\implies\phi(x+1)\right)\right)\implies\forall x\phi(x)$.
For example, the axiomatization I came up with whittles the finite list on this wikipedia page together with the axiom scheme of well-ordering as follows:


*

*Axiom 4 ($\forall x\forall y (xy=yx)$)  can be replaced with the second distributive law $\forall x\forall y\forall z \left((x+y)z=xz+yz\right)$.

*Axiom 12 $\forall x\forall y\forall z \left((0\leq x\wedge y\leq z)\implies (xy\leq xz)\right)$ can be replaced with $\forall x\forall y\left(x\leq y\implies\exists z (x+z=y)\right)$.

*The second half of Axiom 14, $(\forall x(0< x \leq1\implies x=1)$, can be removed.

 A: I can’t say I understand the rationale for using minimization instead of induction, but the following works:


*

*$x+0=x$

*$x+S(y)=S(x+y)$

*$x\cdot0=0$

*$x\cdot S(y)=x\cdot y+x$

*$x=0\lor\exists y\,x=S(y)$

*$S(x)\le y\to x< y$

*$\phi(x)\to\exists z\,(\phi(z)\land\forall y\,(\phi(y)\to z\le y))$
where in 6 and below, $x< y$ is a short-hand for $x\le y\land x\ne y$.
By applying 7 to the formula $x=u\lor x=v$, we get
$$\tag{8}u\le v\lor v\le u,$$
and specializing to $u=v$ gives
$$\tag{9}u\le u.$$
Since $x=x$ and a fortiori $x\nless x$, 6 implies
$$S(x)\nleq x.\tag{10}$$
We can prove the induction schema
$$\phi(0)\land\forall x\,(\phi(x)\to\phi(S(x)))\to\forall x\,\phi(x)\tag{11}$$
as follows: assume for contradiction $\neg\phi(x)$, and let $x$ be the smallest such, as given by 7. We cannot have $x=0$, hence $x=S(y)$ for some $y$ by 5. Then $\neg\phi(y)$ by the premise of the induction axiom, hence $x=S(y)\le y$ by the minimality of $x$, contradicting 10.
We can prove
$$x\le 0\to x=0\tag{12}$$
by induction on $x$ using 6. Also, 8 and 12 imply
$$0\le x\tag{13}.$$
Finally, assume for contradiction that there are $x,y$ such that
$$x< y< S(x).\tag{$*$}$$
Let $x$ be the smallest for which such a $y$ exist, and let $y$ be the smallest for this $x$. We cannot have $y=0$ by 12, hence $y=S(z)$ for some $z$. We have $z< S(x)$ by 6, but $y\nleq z$ by 10, hence the minimality of $y$ implies $x\nless z$, thus $z\le x$ by 8. If $x=z$, then $y=S(x)$ contradicts the assumption $y< S(x)$. Otherwise $z< x< S(z)$, hence the minimality of $x$ implies $x\le z$, thus $x< z$, a contradiction.
In view of 8, the impossibility of $(*)$ implies the converse of 6:
$$x< y\to S(x)\le y.\tag{14}$$
By the Appendix of http://math.cas.cz/~jerabek/papers/t02.pdf, 1–4,6,11,13,14 imply the remaining axioms of PA.
A: This should probably be a comment, but it will be too long.
Here's an axiomatization.  From the wikipedia page you cite, I replace 1 and 5 with weaker axioms.  I suppress 2,3 4,7, 11, 12 and 15.  I replace 8,9, and 10 with the single assumption of anti-symmetry. I strengthen 13 by replacing implication with a sort of iff. I keep the others. And then I add the well-ordering schema as you state it.  That is, assume:


*

*x + 0 = x

*x + (y + 1) = (x + y) + 1

*x * 0 = 0

*x * (y + 1) = x * y + x

*x ≤ y & y ≤ x $\implies$ x = y  

*x ≤ y $\implies$ $\exists$z (z + x = y)  

*$\exists$z (x + z = y & $\neg$ z = 0) $\implies$ x < y  

*$\neg$ x = 0 $\implies$ 1 ≤ x

*$\neg$ 1 = 0

*$\exists x\phi(x)\implies\exists x\left(\left(\phi(x)\wedge \forall y(\phi(y)\implies x\leq y)\right)\right)$


Prop.  (Induction)  $\left(\phi(0)\wedge\forall x\left(\phi(x)\implies\phi(x+1)\right)\right)\implies\forall x\phi(x)$
Pf:
Suppose $\phi$(0) & $\forall$x($\phi$(x) $\implies$ $\phi$(x+1)). And suppose $\neg\forall$ x $\phi$(x), i.e. $\exists$x$\neg$$\phi$(x).  By 10.
$\neg\phi$(c) & $\forall$y($\neg\phi$(y) $\implies$ c ≤ y)) for some c.  $\neg$ c = 0, so by 8. 1 ≤ c.  By 6. (z + 1) = c for some z. By 7. and 9. z < c. If $\phi$(z) then $\phi$(c) by the induction hypothesis, contradiction.  Hence $\neg\phi$(z). Thus c ≤ z. By 5. z = c, contradiction.  QED.   
Once you have induction you can prove commutativity and associativity of addition and multiplication, and the other Wikipedia axioms should follow.  
I have no idea what is known on this, however (or even whether it is worth knowing).  It may well be possible to assume less.
