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.
  • $\begingroup$ Are you looking for something like: 1/ Induction: From phi(0) & (n)(phi(n) => phi(n+1)) infer (n)phi(n) 2/ x ≤ y iff (there exists z)(z + x = y) 3/ x + 0 = 0 4/ x + (y + 1) = (x + y) + 1 5/ x * 0 = 0 6/ x * (y + 1) = (x * y) + x 7/ There is no ≤ maximal element I think that works... $\endgroup$
    – abo
    May 18 '13 at 14:24
  • $\begingroup$ The question I originally wrote was not the question I meant. I have corrected this: thank you abo. $\endgroup$ May 18 '13 at 23:14
  • $\begingroup$ Have you expressed what you want with the axiom scheme of well-ordering? After all, $\phi(x)$ might assert $x\neq x$, but you don't want to assert that there is an $x$ like that. $\endgroup$ May 18 '13 at 23:30
  • $\begingroup$ I think the statement of well-ordering should probably be $\exists x(\phi(x))\implies \exists x(\phi(x)\wedge\forall y<x(\neg\phi(x)))$, right? $\endgroup$ May 18 '13 at 23:53
  • $\begingroup$ You could make it closer to Vladimir's by saying $\exists x(\phi(x))\implies\exists x(\phi(x)\wedge \forall y(\phi(y)\implies x\leq y))$. That is, if there is any $x$ with $\phi(x)$, then there is a least such $x$. $\endgroup$ May 19 '13 at 1:35

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.


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.