\import{set/suc.tex}
\import{set.tex}

\section{Natural numbers}

\begin{abbreviation}\label{num_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{num_naturals_inductive_set}
    $\naturals$ is an inductive set.
\end{axiom}

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

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

\begin{lemma}\label{num_emptyset_in_naturals}
    $\emptyset\in\naturals$.    
\end{lemma}

\begin{signature}\label{num_addition_is_set}
    $x+y$ is a set.
\end{signature}

\begin{axiom}\label{num_addition_on_naturals}
    $x+y$ is a natural number iff $x$ is a natural number and $y$ is a natural number.
\end{axiom}

\begin{abbreviation}\label{num_zero_is_emptyset}
    $\zero = \emptyset$.
\end{abbreviation}

\begin{axiom}\label{num_addition_axiom_1}
    For all $x \in \naturals$ $x + \zero = \zero + x = x$.
\end{axiom}

\begin{axiom}\label{num_addition_axiom_2}
    For all $x, y \in \naturals$ $x + \suc{y} = \suc{x} + y = \suc{x+y}$.
\end{axiom}

\begin{lemma}\label{num_naturals_is_equal_to_two_times_naturals}
    $\{x+y \mid x \in \naturals, y \in \naturals \} = \naturals$.
\end{lemma}