Reference request: Minimal Axiomatizations of PA over (+,x,<=).

Question

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:

1. 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)$.
2. 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)$.
3. The second half of Axiom 14, $(\forall x(0< x \leq1\implies x=1)$, can be removed.

Answer 1

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

1. $x+0=x$

2. $x+S(y)=S(x+y)$

3. $x\cdot0=0$

4. $x\cdot S(y)=x\cdot y+x$

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

6. $S(x)\le y\to x< y$

7. $\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.

Answer 2

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:

1. x + 0 = x
2. x + (y + 1) = (x + y) + 1
3. x * 0 = 0
4. x * (y + 1) = x * y + x
5. x ≤ y & y ≤ x $\implies$ x = y
6. x ≤ y $\implies$ $\exists$z (z + x = y)
7. $\exists$z (x + z = y & $\neg$ z = 0) $\implies$ x < y
8. $\neg$ x = 0 $\implies$ 1 ≤ x
9. $\neg$ 1 = 0
10. $\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.