1Peano Arithmetic¶
Signature: $\mathbb{N}:\{+, \cdot, S, <, 0\}$ where $+$ and $\cdot$ are binary function symbols, $S$ is a unary function symbol (the "successor" function), $<$ is a binary predicate symbol, and $0$ is a constant symbol.
You can express pretty much anything in this signature, even Fermat's last theorem (although that might take a while).
1.1The Peano axioms¶
 (A1) $\forall x(x + 0 = x)$^{1}
 (A2) $\forall x \forall y (x + Sy = S(x+y))$^{1}
 (M1) $\forall x(x\cdot 0 = 0)$
 (M2) $\forall x \forall y (x \cdot Sy = xy +x)$
 (L) $\forall x \forall y (x < y \iff \exists z (x + z = y \land z \neq 0))$
 (S1) $\forall x (Sx \neq 0)$
 (S2) $\forall x \forall y (Sx = Sy \to x = y)$
1.2Induction¶
Those were the seven basic axioms. We also have in PA the schema of mathematical induction. For each formula $\varphi(x_1, y_1, \ldots y_n)$ we have the following induction axiom:
Let $\bar{y} = (y_1, \ldots, y_n)$. Then $\forall \bar{y} [ (\varphi(0, \bar{y}) \land (\forall x[\varphi(x, \bar{y}) \to \varphi(Sx, \bar{y})]) \to \forall x \varphi(x, \bar{y})]$.
1.3Proofs¶
We will be saying things like $PA \vdash \sigma$. This will mean $\Gamma \vdash \sigma$ for some finite $\Gamma \subseteq PA$.
1.3.1Proving that 2 + 2 = 4¶
Line  Justification 

(1) $SS0 + SS0 = S(SS0 + S0)$  By A2 
(2) $SS0 + S0 = S(SS0 + 0)$  By A2 
(3) $SS0 + 0 = SS0$  By A1 
(4) $S(SS0 + 0) = SSS0$  By (3), and substitution 
(5) $SSS0 + 0 = SSS0$  By A1 
(6) $S(SSS0 + 0) = SSSS0$  By (5), and substitution 
(7) $SS0 + S0 = SSS0$  Transitivity using (2) and (4) 
(8) $S(SS0 + S0) = SSSS0$  By (7), and substitution 
(9) $SS0 + SS0 = SSSS0$  Transitivity using (1) and (8) 
Incidentally, here's another way to define the even numbers: $\exists x_2(SS0 \cdot x_2 = x)$ (using $SS0$ since 2 is not an object in this language, lol (except as a subscript)).
1.4A proof using the induction axiom¶
Proposition: $\forall x (x = 0 \lor \exists y (x = Sy))$
To show this, we use the induction axiom $[\varphi(0) \land \forall x (\varphi(x) \to \varphi(Sx))] \to \forall x \varphi(x)$.
We have to show $\varphi(0)$ and $\forall (\varphi(x) \to \varphi(Sx))$
Basis step:
$0 = 0 \lor \exists y (0 = Sy)$
Induction step:
Now suppose $\varphi(x)$; we have to show $\varphi(Sx)$. i.e $Sx = 0 \lor \exists y (Sx = Sy)$. This is true since $Sx = Sy$
This shows:
$PA \vdash \varphi(x) \rightarrow \varphi(Sx)$
$PA \vdash \forall x(\varphi(x) \rightarrow \varphi(Sx))$
So $PA \vdash \forall x \varphi(x)$
1.5Another proof by induction¶
Prove that $\forall x \forall y \forall z [x + (y + z) = (x + y) + z]$ by induction on $z$.
Induction axiom to use:
$\forall y_1 \forall y_2 [y_1 + (y_2 +0) = (y_1 + y_2) + 0 \land \forall x(y_1 + (y_2 +x) = (y_1 + y_2) + x \rightarrow y_1 + (y_2 +Sx) = (y_1 + y_2) + Sx \land \forall x(y_1 + (y_2 +x) = (y_1 + y_2) + x]$
Basis step:
 $y_2 + 0 = y_2$ by A1
 $y_1 + (y_2 + 0) = y_1 + y_2$ by subst. on 1
 $(y_1 + y_2) + 0 = y_1 + y_2$ by A1
 $y_1 + (y_2 + 0) = (y_1 + y_2) + 0$ by trans 2,3
Induction step:
5. $y_1 + (y_2 + x) = (y_1 + y_2) + x$ by IH
6. $y_2 + Sx = S(y_2 + x)$ by A1
7. $y1 = (y2 + Sx) = y_1 + S(y_2 = x)$ by subst.
8. $y_1 + S(y_2 + x) = S(y_1 + (y_2 +x))$ by A2
9. $S(y_1+(y_2+x)) = S((y_1+y_2) + x)$ by IH and subst.
10. $S((y_1+y_2)+x) = (y_1+y_2)+Sx$ by A2
11. $y_1 + (y_2 + Sx) = (y_1 + y_2) + Sx$ by trans
12. $PA \vdash IH \rightarrow 11$ by deduction
13. $PA \vdash \forall x(IH \rightarrow 11)$ $\forall$intro
14. $PA \vdash \forall x(y_1+ (y_2 + x) = (y_1 + y_2) + x)$ by induction
15. $PA \vdash \forall y_1, \forall y_2, \forall x(y_1+ (y_2 + x) = (y_1 + y_2) + x)$

Not strictly logical axioms; only true for $\mathbb{N}$. ↩