Definition:Minimal Arithmetic

From ProofWiki
Jump to navigation Jump to search

Definition

Minimal arithmetic is the set $Q$ of theorems of the recursive set of sentences in the language of arithmetic containing exactly:

\((\text M 1)\)   $:$     \(\displaystyle \forall x:\) \(\displaystyle \map s x \ne 0 \)             
\((\text M 2)\)   $:$     \(\displaystyle \forall x, y:\) \(\displaystyle \map s x = \map s y \implies x = y \)             
\((\text M 3)\)   $:$     \(\displaystyle \forall x:\) \(\displaystyle x + 0 = x \)             
\((\text M 4)\)   $:$     \(\displaystyle \forall x, y:\) \(\displaystyle x + \map s y = \map s {x + y} \)             
\((\text M 5)\)   $:$     \(\displaystyle \forall x:\) \(\displaystyle x \cdot 0 = 0 \)             
\((\text M 6)\)   $:$     \(\displaystyle \forall x, y:\) \(\displaystyle x \cdot \map s y = \paren {x \cdot y} + x \)             
\((\text M 7)\)   $:$     \(\displaystyle \forall x:\) \(\displaystyle \neg x < 0 \)             
\((\text M 8)\)   $:$     \(\displaystyle \forall x, y:\) \(\displaystyle x < \map s y \iff \paren {x < y \lor x = y} \)             
\((\text M 9)\)   $:$     \(\displaystyle \forall x:\) \(\displaystyle 0 < x \iff x \ne 0 \)             
\((\text M 10)\)   $:$     \(\displaystyle \forall x, y:\) \(\displaystyle \map s x < y \iff \paren {x < y \land y \ne \map 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.