PA

Peano Arithmetic (PA) is the restriction of Peano's axioms to a first order theory of arithmetic. The only change is that the induction axiom is replaced by induction restricted to arithmetic formulas:

$$\phi(0)\wedge \forall x(\phi(x)\rightarrow\phi(x'))\rightarrow \forall x\phi(x)) \text{where }\phi\text{ is arithmetical}$$

Note that this replaces the single, second-order, axiom of induction with a countably infinite schema of axioms.

Appropriate axioms defining $+$ , $\cdot$ , and $<$ are included. A full list of the axioms of PA looks like this (although the exact list of axioms varies somewhat from source to source):

• $\forall x (x'\neq 0)$ ($0$ is the first number)
• $\forall x,y (x'=y'\rightarrow x=y)$ (the successor function is one-to-one)
• $\forall x (x+0=x)$ ($0$ is the additive identity)
• $\forall x,y(x+y'=(x+y)')$ (addition is the repeated application of the successor function)
• $\forall x(x\cdot 0=0)$
• $\forall x,y(x\cdot(y')=x\cdot y+x)$ (multiplication is repeated addition)
• $\forall x(\neg (x<0))$ ($0$ is the smallest number)
• $\forall x,y(x<y'\leftrightarrow x<y\vee x=y)$
• $\phi(0)\wedge \forall x(\phi(x)\rightarrow\phi(x'))\rightarrow \forall x\phi(x)) {where }\phi{ is arithmetical}$