\documentclass[../arithmetic.tex]{subfiles}

\begin{document}
  \chapter{Addition}\label{chapter:addition}

  \filename{arithmetic/sections/03_addition.ftl.tex}

  \begin{forthel}
    %[prove off][check off]

    [readtex \path{arithmetic/sections/02_recursion.ftl.tex}]

    %[prove on][check on]
  \end{forthel}


  \section{Definition of addition}

  \begin{forthel}
    \begin{lemma}\printlabel{ARITHMETIC_03_722195546374144}
      There exists a $\varphi : \Nat \times \Nat \to \Nat$ such
      that for all $n \in \Nat$ we have $\varphi(n,0) = n$ and
      $\varphi(n,\succ(m)) = \succ(\varphi(n,m))$ for all $m \in \Nat$.
    \end{lemma}
    \begin{proof}
      Take $A = [\Nat \to \Nat]$.
      Define $a(n) = n$ for $n \in \Nat$.
      Then $A$ is a set and $a \in A$.

      [skipfail on] % Wrong proof task %!!
      Define $f(g) = \fun n \in \Nat. \succ(g(n))$ for $g \in A$.
      [skipfail off]

      Then $f : A \to A$.
      Indeed $f(g)$ is a map from $\Nat$ to $\Nat$ for any $g \in A$.
      Consider a $\psi : \Nat \to A$ such that $\psi$ is recursively defined by
      $a$ and $f$ (by \cref{ARITHMETIC_02_2489427471368192}).
      Define $\varphi(n,m) = \psi(m)(n)$ for $(n,m) \in \Nat \times \Nat$.
      Then $\varphi$ is a map from $\Nat \times \Nat$ to $\Nat$.

      (1) For all $n \in \Nat$ we have $\varphi(n,0) = n$. \\
      Proof.
        Let $n \in \Nat$.
        Then $\varphi(n,0)
          = \psi(0)(n)
          = a(n)
          = n$.
      Qed.

      (2) For all $n, m \in \Nat$ we have $\varphi(n, \succ(m)) =
      \succ(\varphi(n,m))$. \\
      Proof.
        Let $n, m \in \Nat$.
        Then $\varphi(n, \succ(m))
          = \psi(\succ(m))(n)
          = f(\psi(m))(n)
          = \succ(\psi(m)(n))
          = \succ(\varphi(n,m))$.
      Qed.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{lemma}\printlabel{ARITHMETIC_04_2637025605844992}
      Let $\varphi, \varphi' : \Nat \times \Nat \to \Nat$.
      Assume that for all $n \in \Nat$ we have $\varphi(n,0) = n$ and
      $\varphi(n,\succ(m)) = \succ(\varphi(n,m))$ for all $m \in \Nat$.
      Assume that for all $n \in \Nat$ we have $\varphi'(n,0) = n$ and
      $\varphi'(n,\succ(m)) = \succ(\varphi'(n,m))$ for all $m \in \Nat$.
      Then $\varphi = \varphi'$.
    \end{lemma}
    \begin{proof}
      Define $\Phi = \{ m \in \Nat \mid \varphi(n,m) = \varphi'(n,m)$ for
      all $n \in \Nat \}$.

      (1) $0 \in \Phi$.
      Indeed $\varphi(n,0) = n = \varphi'(n,0)$ for all $n \in \Nat$.

      (2) For all $m \in \Phi$ we have $\succ(m) \in \Phi$. \\
      Proof.
        Let $m \in \Phi$.
        Then $\varphi(n,m) = \varphi'(n,m)$ for all $n \in \Nat$.
        Hence $\varphi(n, \succ(m))
          = \succ(\varphi(n,m))
          = \succ(\varphi'(n,m))
          = \varphi(n, \succ(m))$
        for all $n \in \Nat$.
      Qed.

      Thus $\Phi$ contains every natural number.
      Therefore $\varphi(n,m) = \varphi'(n,m)$ for all $n, m \in \Nat$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_03_4372222701469696}
      $\add$ is the map from $\Nat \times \Nat$ to $\Nat$ such that for all
      $n \in \Nat$ we have $\add(n,0) = n$ and $\add(n,\succ(m)) =
      \succ(\add(n,m))$ for all $m \in \Nat$.
    \end{definition}

    Let $n + m$ stand for $\add(n,m)$.
    Let the sum of $n$ and $m$ stand for $n + m$.
  \end{forthel}

  \begin{forthel}
    \begin{lemma}\printlabel{ARITHMETIC_03_3886414804549632}
      Let $n, m$ be natural numbers.
      Then $(n,m) \in \dom(\add)$.
    \end{lemma}
  \end{forthel}

  \begin{forthel}
    \begin{lemma}\printlabel{ARITHMETIC_03_5964925614686208}
      Let $n, m$ be natural numbers.
      Then $n + m$ is a natural number.
    \end{lemma}
  \end{forthel}

  \begin{forthel}
    \begin{lemma}\printlabel{ARITHMETIC_03_777009668030464}
      Let $n$ be a natural number.
      Then $\succ(n) = n + 1$.
    \end{lemma}
  \end{forthel}

  \begin{forthel}
    \begin{lemma}\printlabel{ARITHMETIC_03_4827955356237824}
      Let $n$ be a natural number.
      Then $n + 0 = n$.
    \end{lemma}
  \end{forthel}

  \begin{forthel}
    \begin{lemma}\printlabel{ARITHMETIC_03_1031280145727488}
      Let $n, m$ be natural numbers.
      Then $n + (m + 1) = (n + m) + 1$.
    \end{lemma}
  \end{forthel}


  \section{The Peano axioms and recursion, revisited}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_03_3170769680990208}
      Let $n, m$ be natural numbers.
      If $n + 1 = m + 1$ then $n = m$.
    \end{proposition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_03_1101538491629568}
      Let $n$ be a natural number.
      Then $n + 1 \neq 0$.
    \end{proposition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}[Induction]\printlabel{ARITHMETIC_03_647949900054528}
      Let $A$ be a class.
      Assume $0 \in A$.
      Assume that for all $n \in \Nat$ if $n \in A$ then $n + 1 \in A$.
      Then $A$ contains every natural number.
    \end{proposition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}
      Let $a$ be an object and $f$ be a map.
      Let $\varphi$ be a map from $\Nat$ to $\dom(f)$.
      $\varphi$ is recursively defined by $a$ and $f$ iff $\varphi(0) = a$ and
      $\varphi(n + 1) = f(\varphi(n))$ for every $n \in \Nat$.
    \end{proposition}
  \end{forthel}


  \section{Computation laws}

  \subsection*{Associativity}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_03_3235893452210176}
      Let $n, m, k$ be natural numbers.
      Then \[ n + (m + k) = (n + m) + k. \]
    \end{proposition}
    \begin{proof}
      Define $\Phi = \{ k' \in \Nat \mid n + (m + k') = (n + m) + k' \}$.

      (1) $0$ is contained in $\Phi$.
      Indeed $n + (m + 0) = n + m = (n + m) + 0$.

      (2) For all $k' \in \Phi$ we have $k' + 1 \in \Phi$. \\
      Proof.
        Let $k' \in \Phi$.
        Then $n + (m + k') = (n + m) + k'$.
        Hence
        \[  n + (m + (k' + 1))        \]
        \[    = n + ((m + k') + 1)    \]
        \[    = (n + (m + k')) + 1    \]
        \[    = ((n + m) + k') + 1    \]
        \[    = (n + m) + (k' + 1).   \]
        Thus $k' + 1 \in \Phi$.
      Qed.

      Thus every natural number is an element of $\Phi$.
      Therefore $n + (m + k) = (n + m) + k$.
    \end{proof}
  \end{forthel}


  \subsection*{Commutativity}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_03_4029553232052224}
      Let $n, m$ be natural numbers.
      Then \[ n + m = m + n. \]
    \end{proposition}
    \begin{proof}
      Define $\Phi = \{ m' \in \Nat \mid n + m' = m' + n \}$.

      (1) $0$ is an element of $\Phi$. \\
      Proof.
        Define $\Psi = \{ n' \in \Nat \mid n' + 0 = 0 + n' \}$.

        (1a) $0$ belongs to $\Psi$.

        (1b) For all $n' \in \Psi$ we have $n' + 1 \in \Psi$. \\
        Proof.
          Let $n' \in \Psi$.
          Then $n' + 0 = 0 + n'$.
          Hence
          \[  (n' + 1) + 0        \]
          \[    = n' + 1          \]
          \[    = (n' + 0) + 1    \]
          \[    = (0 + n') + 1    \]
          \[    = 0 + (n' + 1).   \]
        Qed.

        Hence every natural number belongs to $\Psi$.
        Thus $n + 0 = 0 + n$.
        Therefore $0$ is an element of $\Phi$.
      Qed.

      Let us show that (2) $n + 1 = 1 + n$. \\
      Proof.
        Define $\Theta = \{ n' \in \Nat \mid n' + 1 = 1 + n' \}$.

        (2a) $0$ is an element of $\Theta$.

        (2b) For all $n' \in \Theta$ we have $n' + 1 \in \Theta$. \\
        Proof.
          Let $n' \in \Theta$.
          Then $n' + 1 = 1 + n'$.
          Hence
          \[  (n' + 1) + 1        \]
          \[    = (1 + n') + 1    \]
          \[    = 1 + (n' + 1).   \]
          Thus $n' + 1 \in \Theta$.
        Qed.

        Thus every natural number belongs to $\Theta$.
        Therefore $n + 1 = 1 + n$.
      Qed.

      (3) For all $m' \in \Phi$ we have $m' + 1 \in \Phi$. \\
      Proof.
        Let $m' \in \Phi$.
        Then $n + m' = m' + n$.
        Hence
        \[  n + (m'  + 1)       \]
        \[    = (n + m') + 1    \]
        \[    = (m' + n) + 1    \]
        \[    = m' + (n + 1)    \]
        \[    = m' + (1 + n)    \]
        \[    = (m' + 1) + n.   \]
        Thus $m' + 1 \in \Phi$.
      Qed.

      Thus every natural number is an element of $\Phi$.
      Therefore $n + m = m + n$.
    \end{proof}
  \end{forthel}


  \subsection*{Cancellation}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_03_3137702874578944}
      Let $n, m, k$ be natural numbers.
      Then \[ n + k = m + k \implies n = m. \]
    \end{proposition}
    \begin{proof}
      Define $\Phi = \{ k' \in \Nat \mid$ if $n + k' = m + k'$ then $n = m \}$.

      (1) $0$ is an element of $\Phi$.

      (2) For all $k' \in \Phi$ we have $k' + 1 \in \Phi$. \\
      Proof.
        Let $k' \in \Phi$.
        Suppose $n + (k' + 1) = m + (k' + 1)$.
        Then $(n + k') + 1 = (m + k') + 1$.
        Hence $n + k' = m + k'$.
        Thus $n = m$.
      Qed.

      Therefore every natural number is an element of $\Phi$.
      Consequently if $n + k = m + k$ then $n = m$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{corollary}\printlabel{ARITHMETIC_03_8445946379632640}
      Let $n, m, k$ be natural numbers.
      Then \[ k + n = k + m \implies n = m. \]
    \end{corollary}
    \begin{proof}
      Assume $k + n = k + m$.
      We have $k + n = n + k$ and $k + m = m + k$.
      Hence $n + k = m + k$.
      Thus $n = m$.
    \end{proof}
  \end{forthel}


  \subsection*{Zero sums}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_03_3520602170195968}
      Let $n, m$ be natural numbers.
      If $n + m = 0$ then $n = 0$ and $m = 0$.
    \end{proposition}
    \begin{proof}
      Assume $n + m = 0$.
      Suppose $n \neq 0$ or $m \neq 0$.
      Then we can take a $k \in \Nat$ such that $n = k + 1$ or $m = k + 1$.
      Hence there exists a natural number $l$ such that
      $n + m
        = l + (k + 1)
        = (l + k) + 1
        \neq 0$.
      Contradiction.
    \end{proof}
  \end{forthel}
\end{document}
