From 6eea98cf3e66a07251e6370ea948898799d5055b Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 13 Apr 2024 13:01:14 +0200
Subject: first formalisation of addition on naturals

We try to Implement the Addition on natural numbers by a relation on N \times N to N such that some of the axioms of the addition holds
---
 latex/naproche.sty |  2 ++
 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} 
+
+
+
-- 
cgit v1.2.3