blob: 849c610ffb931765c8c3f3975200b17ced3d6fab (
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
51
52
53
54
55
56
57
|
\import{set/suc.tex}
\import{set.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}
\begin{lemma}\label{emptyset_in_naturals}
$\emptyset\in\naturals$.
\end{lemma}
%\begin{abbreviation}\label{zero_is_emptyset}
% $0 = \emptyset$.
%\end{abbreviation}
%\begin{definition}\label{additionpair}
% $x$ is an Additionpair iff $x \in ((\naturals\times \naturals)\times \naturals)$.
%\end{definition}
%\begin{lemma}\label{zero_is_in_naturals}
% Let $n\in \naturals$. $((n, \emptyset), n)$ is an Additionpair.
%\end{lemma}
%\begin{definition}\label{valid_additionpair}
% $x$ is a vaildaddition iff there exist $n \in \naturals$ we have $x = ((0, n), n)$.
%\end{definition}
\begin{axiom}\label{addpair_set}
$\addpair$ is a set.
\end{axiom}
\begin{axiom}\label{addition_naturals}
$x \in \addpair$ iff $x \in ((\naturals\times \naturals)\times \naturals)$ and there exist $n \in \naturals$ such that $x = ((n, \emptyset), n)$.
\end{axiom}
|
