nLab Peano arithmetic

Idea

Peano arithmetic refers to a theory which formalizes arithmetic operations on the natural numbers $\mathbb{N}$ and their properties. There is a first-order Peano arithmetic and a second-order Peano arithmetic, and one may speak of Peano arithmetic in higher-order type theory.

As first-order logic has certain syntactic and model-theoretic advantages over second-order logic, and has been much further developed, the default notion of Peano arithmetic is usually taken to be the first-order one. However, we will describe both the first- and second-order notions. Note that Peano’s original treatment was second-order.

Second-order Peano arithmetic

Against a fixed background of “sets” (which we consider categorically, e.g., a model of ETCS, or even just any topos), Peano arithmetic is formalized by stipulating a set $N$ with an element $0: 1 \to N$ and an unary function $s: N \to N$, subject to the following axioms:

• $\forall_x \neg s(x) = 0$;

• $\forall_{x, y} s(x) = s(y) \Rightarrow x = y$;

• (Second-order induction) $\forall_{I \subseteq N} [0 \in I \wedge (\forall_x x \in I \Rightarrow s(x) \in I] \Rightarrow I = N$.

Regarding $N$ as an algebra of an endofunctor $F(X) = 1 + X$, the first two axioms say that the structure map $(0, s): 1 + N \to N$ is monic, and the induction axiom says that the only $F$-subalgebra of $N$ is $N$ itself. (In particular, $(0, s): F N \to N$ is tautologically an $F$-algebra map where $F N$ is given the $F$-algebra structure $F(0, s): F F N \to F N$. Being monic, the subalgebra $(0, s): F N \to N$ is an isomorphism, by induction.)

It may be shown that these properties determine $N$ up to isomorphism (one says second-order Peano arithmetic is ‘categorical’, but this is not at all related to the notion of category), and moreover:

Proposition

In a topos, an object which satisfies the Peano axioms is a natural numbers object (and natural numbers objects satisfy the Peano axioms).

This is a special case of a much more general result which is part of the general theory of recursion and well-founded coalgebras:

Theorem

If $\mathbf{E}$ is a topos and $F: \mathbf{E} \to \mathbf{E}$ is a taut functor, then any $F$-algebra $X$ whose structure map $\xi: F X \to X$ is monic and for which the only $F$-subalgebra of $X$ is $X$ itself is an initial $F$-algebra.

First-order Peano arithmetic

Here we cannot quantify over subsets, as in the second-order induction scheme, and the initial algebra techniques that can be used to manufacture addition and multiplication do not apply. Instead, addition and multiplication need to be built into the signature. Induction becomes an induction scheme over formulas in the language generated by the signature.

Thus, the signature of first-order Peano arithmetic consists of a constant $0$, an unary function symbol $s$, and binary function symbols $+, \cdot$. The Peano axioms are

1. $\forall_x \neg s(x) = 0$;

2. $\forall_{x, y} s(x) = s(y) \Rightarrow x = y$;

3. $\forall_x \left( x = 0 \vee \exists_y x = s(y) \right)$;

4. $\forall_x x + 0 = x$,

5. $\forall_{x, y} x + s(y) = s(x+y)$;

6. $\forall_x x \cdot 0 = 0$;

7. $\forall_{x, y} x \cdot s(y) = x \cdot y + x$;

8. (Induction scheme) For all formulas $\phi(x, y_1, \ldots, y_k) = \phi(x; \vec{y})$ with $k+1$ free variables,

   $$\forall_{y_1, \ldots, y_k} [\phi(0, \vec{y}) \wedge \forall_x (\phi(x; \vec{y}) \Rightarrow \phi(s(x); \vec{y})] \Rightarrow \forall_z \phi(z, \vec{y}).$$

The third axiom is actually redundant, being an instance of the induction scheme (take $\phi(x) = [x = 0 \vee \exists_y x = s(y)]$). We include it because it is needed for weaker systems of arithmetic in which the induction schema is curtailed or dropped, notably Robinson arithmetic.

By the Lowenheim-Skolem theorem, there are "nonstandard" models of any infinite cardinality of Peano arithmetic, all of them elementarily embedding the standard model of arithmetic.

Related concepts

• Robinson arithmetic

• Heyting arithmetic

• nonstandard model of arithmetic

• Nelson arithmetic

References

Named after Giuseppe Peano; originating in

• Richard Dedekind, Was sind und was sollen die Zahlen? (1888) [scan: pdf, doi:10.1007/978-3-663-02788-1]

• Richard Dedekind (transl. by W. Beman), The nature and meaning of numbers, Chapter II in: Essays on the Theory of Numbers, Chicago (1901) [Project Gutenberg, pdf]

• Giuseppe Peano, Arithmetices principia, nova methodo exposita, [Wikipedia]

Review:

• David E. Joyce, The Dedekind/Peano Axioms (2005) [pdf]

• Wikipedia, Peano axioms