blob: 529ba54329fdd7e4e41af7ba035c9e0f1fc411fb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
\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}
|
