Over the years, a consensus has arisen that the obviously true claims about the natural numbers can be formalised in what has come to be known as Peano Arithmetic, or PA for short, named after the Italian mathematician Giuseppe Peano. This is a certain first-order theory whose main axiom states a form of induction for natural numbers.
PA is formulated in a first-order language that has the constant $0$ together with the unary successor function s and the identity predicate. It also contains successor function the binary function symbols + and $\times$, but we think of $0$ and $s$ as primitive, while the meanings of $+$ and $\times$ will be completely defined by axioms of PA. Intuitively, the successor function applied to any number $n$ gives us the next greatest number (what we would normally write as $n + 1$). So $s(0)$ denotes $1$, $s(s(0))$ denotes $2$, and so forth.
> [!NOTE] Definition (Peano Axioms in $L_{2}$)
> Here are the first six axioms of Peano Arithmetic:
> 1. $0$ is not the successor of any element: $\forall x(s(x)\neq 0).$
> 2. Two numbers of which the successors are equal are themselves equal: $\forall x \forall y (s(x)=s(y)\to x=y)$
> 3. $0$ is the additive identity: $\forall x(x+0=x)$
> 4. The result of adding the successor of $n$ to $m$ is the successor of the result of adding $n$ to $m$: $\forall x\forall y[x+s(y)=s(x+y)]$
> 5. The result of multiplying by $0$ is $0$ $\forall(x \times 0=0)$
> 6. Distributivity $\forall x \forall y [x \times s(y) = (x \times y)+x]$
> 7. **[[First-order induction axiom scheme]]** $[Q(0) \land \forall x \, (Q(x)\to Q(s(x)))]\to \forall x\,Q(x)$
# Properties
**Undecidability & Incompleteness**: Peano Arithmetic is remarkably powerful. Indeed, almost all of the theorems mathematicians have proven about the natural numbers can be proven in pa. There are, however, truths about the natural numbers that cannot be proven from pa. Not only that, but any attempt to set down a list of first- order axioms true of the natural numbers must, in some sense, fail. We will discuss this result, known as [[Gödel’s Incompleteness Theorem]].