blob: 18c24f9ea80f92567f18be9c22ab3d49cb1187e2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
\import{set/suc.tex}
\import{set.tex}
\section{Natural numbers}
\begin{abbreviation}\label{num_inductive_set}
$A$ is an inductive set iff it is not the case that if $\emptyset\in A$,
then it is not the case that for all $a$ we have if $a\in A$,
then $\suc{a}\in A$.
\end{abbreviation}
\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}
If $x$ and $y$ are natural numbers, then $x + 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}
\begin{proof}
We have for all $z\in \{x+y \mid x \in \naturals, y \in \naturals \}$
we have $z\in\naturals$ by \cref{num_addition_on_naturals}.
We have for all $z\in\naturals$
we have $z\in \{x+y \mid x \in \naturals, y \in \naturals \}$
by \cref{num_addition_axiom_1,num_emptyset_in_naturals}.
Follows by set extensionality.
\end{proof}
|
