11,335
pages

Peano arithmetic (also known as first-order arithmetic) is a first-order axiomatic theory over the natural numbers.

## Language

The language of first-order arithmetic consists of the language of predicate logic extended by the following:

• Constant symbol $$0$$, called zero
• Relation symbol $$=$$, called equality
• Unary function symbol $$S(x)$$, called successor
• Two binary function symbols, $$+(a,b),\cdot(a,b)$$, called addition and multiplication respectively, and often denoted by $$a+b,a\cdot b$$.

## Axioms

1. $$\forall n:0\neq S(n)$$ - zero isn't a successor of any natural number.
2. $$\forall n,m: S(n)=S(m)\Rightarrow n=m$$ - two numbers with equal successors are equal themselves, so $$S(x)$$ is an injective function.
3. $$\forall n: n+0=n$$
4. $$\forall n,m: n+S(m)=S(n+m)$$ - this and previous axiom state inductive properties of addition.
5. $$\forall n: n\cdot 0=0$$
6. $$\forall n,m: n\cdot S(m)=n\cdot m+n$$ - this and previous axiom state inductive properties of multiplication.
7. For every first-order formula $$\varphi(x)$$: $$(\varphi(0)\land(\forall n:\varphi(n)\Rightarrow\varphi(S(n)))\Rightarrow\forall n:\varphi(n)$$ - this is so called axiom schema of induction, which states that if some property $$\varphi$$ holds for zero, and if any number $$n$$ posseses this property, then so does its successor, then this property holds for every natural number.

## Analysis

We assume consistency, which is not proven but strongly believed. PA can prove many everyday facts about the natural numbers, and considering Friedman's grand conjecture,[1] it may even be more than enough.

Some examples of googological functions that eventually dominate all functions provably recursive in PA are the Kirby-Paris hydra, Beklemishev's worms, and Goodstein sequences.

PA has proof-theoretic ordinal $$\varepsilon_0$$.