Definition:Minimal Arithmetic
From ProofWiki
Definition
Please fix formatting and $\LaTeX$ errors and inconsistencies.
It may also need to be brought up to our standard house style.
If you have done this or know it has been done, please remove {{Tidy}} from the code.
Minimal arithmetic is the set $Q$ of theorems of the recursive set of sentences in the language of arithmetic containing exactly:
- $\forall x (x' \neq 0)$
- $\forall x \forall y (s(x)=s(y) \rightarrow x=y)$
- $\forall x (x+0 = x)$
- $\forall x \forall y (x+s(y) = s(x+y))$
- $\forall x (x\cdot 0 = 0)$
- $\forall x \forall y (x\cdot s(y) = (x\cdot y)+x)$
- $\forall x (\neg x < 0)$
- $\forall x \forall y (x < s(y) \leftrightarrow (x < y \vee x = y))$
- $\forall x (0 < x \leftrightarrow x \neq 0)$
- $\forall x \forall y (s(x) < y \leftrightarrow (x < y \wedge y \neq s(x)))$
Note
These are just the usual axioms of arithmetic, except for the inductive axioms.
Note in particular that this is a finite list.
