Adding the first formalisation of reals

1 files changed, 23 insertions, 18 deletions

diff --git a/library/nat.tex b/library/nat.tex
index 849c610..ac9a141 100644
--- a/library/nat.tex
+++ b/library/nat.tex
@@ -24,34 +24,39 @@
     $\emptyset\in\naturals$.    
 \end{lemma}
 
-%\begin{abbreviation}\label{zero_is_emptyset}
-%    $0 = \emptyset$.
-%\end{abbreviation}
+\begin{signature}\label{addition_is_set}
+    $x+y$ is a set.
+\end{signature}
+
+\begin{axiom}\label{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{zero_is_emptyset}
+    $\zero = \emptyset$.
+\end{abbreviation}
+
+\begin{axiom}\label{addition_axiom_1}
+    For all $x \in \naturals$ $x + \zero = \zero + x = x$.
+\end{axiom}
+
+\begin{axiom}\label{addition_axiom_2}
+    For all $x, y \in \naturals$ $x + \suc{y} = \suc{x} + y = \suc{x+y}$.
+\end{axiom}
+
+\begin{lemma}\label{naturals_is_equal_to_two_times_naturals}
+    $\{x+y \mid x \in \naturals, y \in \naturals \} = \naturals$.
+\end{lemma}
 
-%\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}