diff options
| -rw-r--r-- | latex/naproche.sty | 2 | ||||
| -rw-r--r-- | library/nat.tex | 40 |
2 files changed, 40 insertions, 2 deletions
diff --git a/latex/naproche.sty b/latex/naproche.sty index 9764693..d975f21 100644 --- a/latex/naproche.sty +++ b/latex/naproche.sty @@ -127,6 +127,8 @@ \newcommand{\Univ}[1]{\fun{Univ}(#1)} \newcommand{\upward}[2]{#2^{\uparrow #1}} \newcommand{\LeftOrb}[2]{#2\cdot #1} +\newcommand{\addpair}{\mathcal{H}} +%\newcommand{\add}[2]{(#1 + #2)} \newcommand\restrl[2]{{% we make the whole thing an ordinary symbol diff --git a/library/nat.tex b/library/nat.tex index 529ba54..849c610 100644 --- a/library/nat.tex +++ b/library/nat.tex @@ -1,5 +1,5 @@ \import{set/suc.tex} - +\import{set.tex} \section{Natural numbers} @@ -17,5 +17,41 @@ \end{axiom} \begin{abbreviation}\label{naturalnumber} - $n$ is a natural number iff $n\in\naturals$. + $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} + + + |