\begin{definition}[Definition:Minimal Arithmetic]
'''Minimal arithmetic''' is the set $Q$ of theorems of the recursive set of sentences in the language of arithmetic containing exactly:
{{begin-axiom}}
{{axiom | n = \text M 1
        | q = \forall x
        | m = \map s x \ne 0
}}
{{axiom | n = \text M 2
        | q = \forall x, y
        | m = \map s x = \map s y \implies x = y
}}
{{axiom | n = \text M 3
        | q = \forall x
        | m = x + 0 = x
}}
{{axiom | n = \text M 4
        | q = \forall x, y
        | m = x + \map s y = \map s {x + y}
}}
{{axiom | n = \text M 5
        | q = \forall x
        | m = x \cdot 0 = 0
}}
{{axiom | n = \text M 6
        | q = \forall x, y
        | m = x \cdot \map s y = \paren {x \cdot y} + x
}}
{{axiom | n = \text M 7
        | q = \forall x
        | m = \neg x < 0
}}
{{axiom | n = \text M 8
        | q = \forall x, y
        | m = x < \map s y \iff \paren {x < y \lor x = y}
}}
{{axiom | n = \text M 9
        | q = \forall x
        | m = 0 < x \iff x \ne 0
}}
{{axiom | n = \text M 10
        | q = \forall x, y
        | m = \map s x < y \iff \paren {x < y \land y \ne \map s x}
}}
{{end-axiom}}
\end{definition}