nLab Peano arithmetic

Redirected from "Dedekind-Peano axioms".
Contents

Context

Model theory

Arithmetic

Contents

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 NN with an element 0:1N0: 1 \to N and an unary function s:NNs: N \to N, subject to the following axioms:

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

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

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

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

It may be shown that these properties determine NN 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 E\mathbf{E} is a topos and F:EEF: \mathbf{E} \to \mathbf{E} is a taut functor, then any FF-algebra XX whose structure map ξ:FXX\xi: F X \to X is monic and for which the only FF-subalgebra of XX is XX itself is an initial FF-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 00, an unary function symbol ss, and binary function symbols +,+, \cdot. The Peano axioms are

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

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

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

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

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

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

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

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

    y 1,,y k[ϕ(0,y) x(ϕ(x;y)ϕ(s(x);y)] zϕ(z,y).\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 ϕ(x)=[x=0 yx=s(y)]\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.

In addition, the additional parameters y\vec{y} are not needed in the induction scheme; adding the induction scheme for first-order formulae ϕ(x)\phi(x) where the only parameter is xx:

  • (Induction scheme) For all formulas ϕ(x)\phi(x),
    [ϕ(0) x(ϕ(x)ϕ(s(x))] zϕ(z).[\phi(0) \wedge \forall_x (\phi(x) \Rightarrow \phi(s(x))] \Rightarrow \forall_z \phi(z).

results in an equivalent theory to Peano arithmetic. See Parameters in arithmetic induction axiom schemas.

By the Lowenheim-Skolem theorem, there are "nonstandard" models of any infinite cardinality of Peano arithmetic.

Formalization

We present here a formalization of first-order Peano arithmetic in a deduction system using inference rules. Such a formalization is important because first-order Peano arithmetic is needed to formally define the universe levels of the universe hierarchy of Russell universes or Coquand universes in many dependent type theories, such as the dependent type theory in the HoTT book.

First-order Peano arithmetic, as a first-order theory with sorts, consists of the following judgments

  • Γctx\Gamma \; \mathrm{ctx}, that Γ\Gamma is a context

  • ϕprop\phi \; \mathrm{prop}, that ϕ\phi is a proposition,

  • ϕtrue\phi \; \mathrm{true}, that ϕ\phi is a true proposition,

  • AsortA \; \mathrm{sort}, that AA is a sort,

  • aAa \in A, that aa is in sort AA.

In addition, we have rules stating that one could form the empty context, and one could add true proposition judgments and element judgments to the list of contexts:

()ctxΓctxΓPprop(Γ,Ptrue)ctxΓctxΓAsort(Γ,aA)ctx\frac{}{() \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash P \; \mathrm{prop}}{(\Gamma, P \; \mathrm{true}) \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash A \; \mathrm{sort}}{(\Gamma, a \in A) \; \mathrm{ctx}}

We also have rules saying that given a context with a true proposition or element judgment, said judgment holds:

(Γ,Ptrue,Δ)ctx(Γ,Ptrue,Δ)Ptrue(Γ,xA,Δ)ctx(Γ,xA,Δ)xA\frac{(\Gamma, P \; \mathrm{true}, \Delta) \; \mathrm{ctx}}{(\Gamma, P \; \mathrm{true}, \Delta) \vdash P \; \mathrm{true}} \qquad \frac{(\Gamma, x \in A, \Delta) \; \mathrm{ctx}}{(\Gamma, x \in A, \Delta) \vdash x \in A}

In addition, we have the natural deduction inference rules for classical propositional logic:

  • Inference rules for true:
ΓctxΓpropΓctxΓtrue\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \top \; \mathrm{prop}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \top \; \mathrm{true}}
  • Inference rules for false:
ΓctxΓpropΓPpropΓ,truePtrue\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \bot \; \mathrm{prop}} \qquad \frac{\Gamma \vdash P \; \mathrm{prop}}{\Gamma, \bot \; \mathrm{true} \vdash P \; \mathrm{true}}
ΓPpropΓQpropΓPQpropΓPtrueΓQtrueΓPQtrueΓPQtrueΓPtrueΓPQtrueΓQtrue\frac{\Gamma \vdash P \; \mathrm{prop} \quad \Gamma \vdash Q \; \mathrm{prop}}{\Gamma \vdash P \wedge Q \; \mathrm{prop}} \qquad \frac{\Gamma \vdash P \; \mathrm{true} \quad \Gamma \vdash Q \; \mathrm{true}}{\Gamma \vdash P \wedge Q \; \mathrm{true}} \qquad \frac{\Gamma \vdash P \wedge Q \; \mathrm{true}}{\Gamma \vdash P \; \mathrm{true}} \qquad \frac{\Gamma \vdash P \wedge Q \; \mathrm{true}}{\Gamma \vdash Q \; \mathrm{true}}
ΓPpropΓQpropΓPQpropΓPpropΓQpropΓ,PtruePQtrueΓPpropΓQpropΓ,QtruePQtrue\frac{\Gamma \vdash P \; \mathrm{prop} \quad \Gamma \vdash Q \; \mathrm{prop}}{\Gamma \vdash P \vee Q \; \mathrm{prop}} \qquad \frac{\Gamma \vdash P \; \mathrm{prop} \quad \Gamma \vdash Q \; \mathrm{prop}}{\Gamma, P \; \mathrm{true} \vdash P \vee Q \; \mathrm{true}} \qquad \frac{\Gamma \vdash P \; \mathrm{prop} \quad \Gamma \vdash Q \; \mathrm{prop}}{\Gamma, Q \; \mathrm{true} \vdash P \vee Q \; \mathrm{true}}
ΓPpropΓQpropΓ,PQtrueRpropΓ,PtrueRtrueΓ,QtrueRtrueΓ,PQtrueRtrue\frac{\Gamma \vdash P \; \mathrm{prop} \quad \Gamma \vdash Q \; \mathrm{prop} \quad \Gamma, P \vee Q \; \mathrm{true} \vdash R \; \mathrm{prop} \quad \Gamma, P \; \mathrm{true} \vdash R \; \mathrm{true} \quad \Gamma, Q \; \mathrm{true} \vdash R \; \mathrm{true}}{\Gamma, P \vee Q \; \mathrm{true} \vdash R \; \mathrm{true}}
ΓPpropΓQpropΓPQpropΓPpropΓ,PtrueQtrueΓPQtrueΓPQtrueΓ,PtrueQtrue\frac{\Gamma \vdash P \; \mathrm{prop} \quad \Gamma \vdash Q \; \mathrm{prop}}{\Gamma \vdash P \Rightarrow Q \; \mathrm{prop}} \qquad \frac{\Gamma \vdash P \; \mathrm{prop} \quad \Gamma, P \; \mathrm{true} \vdash Q \; \mathrm{true}}{\Gamma \vdash P \Rightarrow Q \; \mathrm{true}} \qquad \frac{\Gamma \vdash P \Rightarrow Q \; \mathrm{true}}{\Gamma, P \; \mathrm{true} \vdash Q \; \mathrm{true}}
ΓPpropΓP(P)true\frac{\Gamma \vdash P \; \mathrm{prop}}{\Gamma \vdash P \vee (P \Rightarrow \bot) \; \mathrm{true}}

First-order Peano arithmetic consists of one sort 𝒩\mathcal{N}:

ΓctxΓ𝒩sort\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathcal{N} \; \mathrm{sort}}

for which it is possible to quantify over elements of 𝒩\mathcal{N}:

ΓctxΓ,x𝒩P(x)propΓx𝒩.P(x)propΓctxΓ,x𝒩P(x)trueΓx𝒩.P(x)trueΓctxΓx𝒩.P(x)trueΓ,x𝒩P(x)true\frac{\Gamma \; \mathrm{ctx} \quad \Gamma, x \in \mathcal{N} \vdash P(x) \; \mathrm{prop}}{\Gamma \vdash \forall x \in \mathcal{N}.P(x) \; \mathrm{prop}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma, x \in \mathcal{N} \vdash P(x) \; \mathrm{true}}{\Gamma \vdash \forall x \in \mathcal{N}.P(x) \; \mathrm{true}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash \forall x \in \mathcal{N}.P(x) \; \mathrm{true}}{\Gamma, x \in \mathcal{N} \vdash P(x) \; \mathrm{true}}
ΓctxΓ,x𝒩P(x)propΓx𝒩.P(x)prop\frac{\Gamma \; \mathrm{ctx} \quad \Gamma, x \in \mathcal{N} \vdash P(x) \; \mathrm{prop}}{\Gamma \vdash \exists x \in \mathcal{N}.P(x) \; \mathrm{prop}}
ΓctxΓ,x𝒩P(x)propΓx𝒩ΓP(x)trueΓx𝒩.P(x)true\frac{\Gamma \; \mathrm{ctx} \quad \Gamma, x \in \mathcal{N} \vdash P(x) \; \mathrm{prop} \quad \Gamma \vdash x \in \mathcal{N} \quad \Gamma \vdash P(x) \; \mathrm{true}}{\Gamma \vdash \exists x \in \mathcal{N}.P(x) \; \mathrm{true}}
ΓctxΓ,x𝒩P(x)propΓ,x𝒩.P(x)trueQpropΓ,x𝒩,P(x)trueQtrueΓ,x𝒩.P(x)trueQtrue\frac{\Gamma \; \mathrm{ctx} \quad \Gamma, x \in \mathcal{N} \vdash P(x) \; \mathrm{prop} \quad \Gamma, \exists x \in \mathcal{N}.P(x) \; \mathrm{true} \vdash Q \; \mathrm{prop} \quad \Gamma, x \in \mathcal{N}, P(x) \; \mathrm{true} \vdash Q \; \mathrm{true}}{\Gamma, \exists x \in \mathcal{N}.P(x) \; \mathrm{true} \vdash Q \; \mathrm{true}}

as well as compare elements of 𝒩\mathcal{N} for propositional equality:

  • Inference rules for propositional equality on 𝒩\mathcal{N}:
ΓctxΓ,x𝒩,y𝒩x=ypropΓctxΓx𝒩.x=xtrue\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x \in \mathcal{N}, y \in \mathcal{N} \vdash x = y \; \mathrm{prop}} \quad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \forall x \in \mathcal{N}.x = x \; \mathrm{true}}
ΓctxΓ,x𝒩,y𝒩P(x,y)propΓ(x𝒩.P(x,x))(x𝒩.y𝒩.x=yP(x,y))true\frac{\Gamma \; \mathrm{ctx} \quad \Gamma, x \in \mathcal{N}, y \in \mathcal{N} \vdash P(x, y) \; \mathrm{prop}}{\Gamma \vdash \left(\forall x \in \mathcal{N}.P(x, x)\right) \Rightarrow \left(\forall x \in \mathcal{N}.\forall y \in \mathcal{N}.x = y \Rightarrow P(x, y)\right) \; \mathrm{true}}

Then we have the axioms and signatures for Peano arithmetic, which are given by the following inference rules:

  • Inference rules for successor:
ΓctxΓ,x𝒩s(x)𝒩\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x \in \mathcal{N} \vdash s(x) \in \mathcal{N}}
ΓctxΓx𝒩.¬(s(x)=0)true\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \forall x \in \mathcal{N}.\neg (s(x) = 0) \; \mathrm{true}}
ΓctxΓx𝒩.y𝒩.(s(x)=s(y))(x=y)true\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \forall x \in \mathcal{N}.\forall y \in \mathcal{N}.(s(x) = s(y)) \Rightarrow (x = y) \; \mathrm{true}}
  • Inference rules for addition:
ΓctxΓ,x𝒩,y𝒩x+y𝒩\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x \in \mathcal{N}, y \in \mathcal{N} \vdash x + y \in \mathcal{N}}
ΓctxΓx𝒩.x+0=xtrue\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \forall x \in \mathcal{N}.x + 0 = x \; \mathrm{true}}
ΓctxΓx𝒩.y𝒩.x+s(y)=s(x+y)true\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \forall x \in \mathcal{N}.\forall y \in \mathcal{N}.x + s(y) = s(x + y) \; \mathrm{true}}
  • Inference rules for multiplication:
ΓctxΓ,x𝒩,y𝒩xy𝒩\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x \in \mathcal{N}, y \in \mathcal{N} \vdash x \cdot y \in \mathcal{N}}
ΓctxΓx𝒩.x0=0true\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \forall x \in \mathcal{N}.x \cdot 0 = 0 \; \mathrm{true}}
ΓctxΓx𝒩.y𝒩.xs(y)=xy+xtrue\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \forall x \in \mathcal{N}.\forall y \in \mathcal{N}.x \cdot s(y) = x \cdot y + x \; \mathrm{true}}
  • Axiom schema of induction:
ΓctxΓ,x𝒩P(x)propΓ(P(0)x𝒩.P(x)P(s(x)))x𝒩.P(x)true\frac{\Gamma \; \mathrm{ctx} \quad \Gamma, x \in \mathcal{N} \vdash P(x) \; \mathrm{prop}}{\Gamma \vdash \left(P(0) \wedge \forall x \in \mathcal{N}.P(x) \Rightarrow P(s(x))\right)\Rightarrow \forall x \in \mathcal{N}.P(x) \; \mathrm{true}}

This concludes the formalization of first-order Peano arithmetic.

References

Named after Giuseppe Peano; originating in

Review:

Last revised on March 18, 2024 at 17:35:25. See the history of this page for a list of all contributions to it.