Peano Axioms

Peano Axioms

The axioms for arithmetic are

• $S(x)\ne 0$.
• $x\ne 0\to \exists y(x=S(y))$.
• $x+0=x$.
• $x+S(y)=S(x+y)$.
• $x\cdot 0=0$.
• $x\cdot S(y)=x\cdot y+x$. Plus the axiom for induction:
• $\left[\phi (0,\bar{y})\wedge \forall x\left(\phi (x,\bar{y})\to \phi (S(x),\bar{y})\right)\right]\to \forall x\phi (x,\bar{y}).$

We can define the binary relation $<$ by

$x<y\text{iff}\exists z(z\ne 0\wedge x+z=y).$

The standard properties for $<$ and its interaction with addition and multiplication can be checked:

• $<$ is a linear ordering,
• $0<x\wedge y<z\to x\cdot y<x\cdot z$,
• $0<x\wedge y<z\to x+y<x+z$,
• etc..

How Strong are the Peano Axioms?

Extremely! All the basic first-order properties of addition, multiplication, exponentiation, etc. can be expressed and proved in PA. Arguably, every result proved in either classical number theory or combinatorics about the natural numbers can be formalized in PA. (Marker, 2024, Chapter 13) Versions of the Prime Number Theorem are expressible and provable in PA. The Riemann Hypothesis has PA equivalent versions, and if true it “probably” also has a PA proof. Fermat’s last Theorem is readily expressed in L. Although its proof uses methods far from PA, it seems probable that it’s proof can, in principle, be done in PA. In fact, there is a major current project within the Lean community to unfold a proof of Fermat’s Last Theorem down to basic Lean assumptions. This would bring one much closer to knowing if there is, in principle, a proof of that theorem from the Peano Axioms. The consensus seems to be that there is indeed such a proof. It is quite difficult to obtain a first-order sentence which is true in N but not provable in PA. We will do this in the proof of Gödel’s Incompleteness Theorem in Chapter 7. There are, however, more recent examples of “natural” first-order mathematical statements, concerning the Hydra Problem and the behaviour of the Goodstein functions, which are true but unprovable from the Peano axioms, and which we will later discuss. See also Goodstein’s Theorem. For interesting related material see Representation of ϵ0 by rooted trees