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, ≤). 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.