\import{set/suc.tex}


\section{Natural numbers}

\begin{abbreviation}\label{inductive_set}
    $A$ is an inductive set iff $\emptyset\in A$ and for all $a\in A$ we have $\suc{a}\in A$.
\end{abbreviation}

\begin{axiom}\label{naturals_inductive_set}
    $\naturals$ is an inductive set.
\end{axiom}

\begin{axiom}\label{naturals_smallest_inductive_set}
    Let $A$ be an inductive set.
    Then $\naturals\subseteq A$.
\end{axiom}

\begin{abbreviation}\label{naturalnumber}
    $n$ is a natural number iff $n\in\naturals$.
\end{abbreviation}