Axioms for the Integers

Branko Ćurgus

In the axioms below we use the standard logical operators: conjunction $\wedge$, disjunction $\vee$, exclusive disjunction $\oplus,$ implication $\Rightarrow,$ universal quantifier $\forall,$ existential quantifier $\exists.$

We also use the standard set notation: set membership $\in$, subset $\subseteq$, equality $=,$ negation of equality $\neq,$ the empty set $\emptyset,$ Cartesian product $\times.$ For singleton sets instead of writing $\{a\} = \{b\}$ we write $a = b$.

The notation $f:A\to B$ stands for a function $f$ which is defined on a set $A$ with the values in $B$.

Axiom 1 below establishes the existence of the addition function defined on $\nZ\times \nZ$ with the values in $\nZ$. It is common to denote the value of $+$ at a pair $(a, b) \in \nZ\times \nZ$ by $a+b$.

Axiom 6 establishes the existence of the multiplication function defined on $\nZ\times \nZ$ with the values in $\nZ$. It is common to denote the value of this function at a pair $(a,b) \in \nZ\times \nZ$ by $a\cdot b$ which is almost always abbreviated as $ab$.

Axiom 12 introduces a strict total order $\ \lt\ $ on $\nZ$.

In Axiom 16 we use the abbreviation $a \leq b$ for the proposition $(a \lt b) \oplus (a=b)$. This axiom is the subtlest of all the axioms.

Axiom 0. (ZE) $\nZ \neq \emptyset$

Axiom 1. (AE) $\exists \ \, +: \nZ \times \nZ \to \nZ$.
Axiom 2. (AA) $\forall\, a \in \nZ \ \ \forall \, b \in \nZ \ \ \forall\, c \in \nZ \quad a+(b+c) = (a+b)+c$
Axiom 3. (AC) $\forall\, a \in \nZ \ \ \forall \, b \in \nZ \quad a+b = b+a$
Axiom 4. (AZ) $\exists\, 0 \in \nZ \ \ \forall\, a \in \nZ \quad 0+a = a$
Axiom 5. (AO) $\forall\, a \in \nZ \ \ \exists\, x \in \nZ \quad a + x = 0$

Axiom 6. (ME) $\exists \ \, \cdot : \nZ \times \nZ \to \nZ$.
Axiom 7. (MA) $\forall\, a \in \nZ \ \ \forall\, b \in \nZ \ \ \forall\, c \in \nZ \quad a(bc) = (ab)c$
Axiom 8. (MC) $\forall\, a \in \nZ \ \ \forall \, b \in \nZ \quad ab = ba$
Axiom 9. (MO) $\exists\, 1 \in \nZ \quad \bigl(1 \neq 0 \bigr) \wedge \bigl( \forall\, a \in \nZ \quad 1\cdot a = a\bigr)$
Axiom 10. (MZ) $\forall\, a \in \nZ \ \ \forall\, b \in \nZ \quad ab = 0 \Rightarrow (a = 0) \vee (b = 0)$

Axiom 11. (DL) $\forall\, a \in \nZ \ \ \forall\, b \in \nZ \ \ \forall\, c \in \nZ \quad a(b+c) = ab + ac$

Axiom 12. (OE) $\forall\, a \in \nZ \ \ \forall\, b \in \nZ \quad (a \lt b) \oplus (a = b) \oplus (b \lt a)$
Axiom 13. (OT) $\forall\, a \in \nZ \ \ \forall\, b \in \nZ \ \ \forall\, c \in \nZ \quad (a \lt b) \wedge (b \lt c) \Rightarrow a \lt c$
Axiom 14. (OA) $\forall\, a \in \nZ \ \ \forall\, b \in \nZ \ \ \forall\, c \in \nZ \quad a \lt b \Rightarrow a + c \lt b + c$
Axiom 15. (OM) $\forall\, a \in \nZ \ \ \forall\, b \in \nZ \ \ \forall\, c \in \nZ \quad (a \lt b) \wedge (0\lt c) \Rightarrow ac \lt bc $

Axiom 16. (WO) $\bigl( S \subseteq \nZ \bigr) \wedge \bigl( S \neq \emptyset \bigr) \wedge \bigl( \forall x \in S \ \ 0 \lt x \bigr) \Rightarrow \bigl( \exists \, m \in S \ \forall x \in S \ \ m \leq x \bigr)$

Explanations for abbreviations: ZE - integers exist, AE - addition exists, AA - addition is associative, AC - addition is commutative, AZ - addition has zero, AO - addition has opposites, ME - multiplication exists, MA - multiplication is associative, MC - multiplication is commutative, MO - multiplication has one, MZ - multiplication respects zero, DL - distributive law, OE - order exists, OT - order is transitive, OA - order respects addition, OM - order respects multiplication, WO - the well-ordering axiom.