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

\begin{document}
  \chapter{Recursion}\label{chapter:recursion}

  \filename{arithmetic/sections/02_recursion.ftl.tex}

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

    [readtex \path{arithmetic/sections/01_natural-numbers.ftl.tex}]

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


  \begin{forthel}
    \begin{definition}\printlabel{ARITHMETIC_02_4608408013504512}
      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(\succ(n)) = f(\varphi(n))$ for every $n \in \Nat$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{theorem}[Dedekind]\printlabel{ARITHMETIC_02_2489427471368192}
      Let $A$ be a set and $a \in A$ and $f : A \to A$.
      Then there exists a $\varphi : \Nat \to A$ that is recursively defined by
      $a$ and $f$.
    \end{theorem}
    \begin{proof}
      Define \[ \Phi = \class{H \in \pow(\Nat \times A) | \classtext{
      $(0, a) \in H$ and for all $n \in \Nat$ and all $x \in A$ if
      $(n, x) \in H$ then $(\succ(n), f(x)) \in H$}}. \]

      Let us show that $\bigcap \Phi \in \Phi$. \\
      Proof.

        (1) $\bigcap \Phi \in \pow(\Nat \times A)$. \\
        Proof.
          We have $\Nat \times A \in \Phi$.
          Hence $\Phi$ is nonempty.
          Any element of $\bigcap \Phi$ is contained in every element of $\Phi$.
          Hence any element of $\bigcap \Phi$ is contained in
          $\Nat \times A$.
          Thus $\bigcap \Phi \subseteq \Nat \times A$.
          $\bigcap \Phi$ is a set.
          Hence $\bigcap \Phi$ is a subset of $\Nat \times A$.
        Qed.

        (2) $(0, a) \in \bigcap \Phi$. \\
        Indeed $(0, a) \in \Nat \times A \in \Phi$.

        (3) For all $n \in \Nat$ and all $x \in A$ if $(n, x) \in
        \bigcap \Phi$ then $(\succ(n), f(x)) \in \bigcap \Phi$. \\
        Proof.
          Let $n \in \Nat$ and $x \in A$.
          Assume $(n, x) \in \bigcap \Phi$.
          Then $(n, x)$ is contained in every element of $\Phi$.
          Hence $(\succ(n), f(x))$ is contained in every element of $\Phi$.
          Thus $(\succ(n), f(x)) \in \bigcap \Phi$.
        Qed.
      Qed.

      Let us show that for any $n \in \Nat$ there exists an $x \in A$ such
      that $(n, x) \in \bigcap \Phi$. \\
      Proof.
        Define $\Psi = \{ n \in \Nat \mid$ there exists an $x \in A$ such that
        $(n, x) \in \bigcap \Phi \}$.

        (1) $0$ is contained in $\Psi$.
        Indeed $(0, a) \in \bigcap \Phi$.

        (2) For all $n \in \Psi$ we have $\succ(n) \in \Psi$. \\
        Proof.
          Let $n \in \Psi$.
          Take an $x \in A$ such that $(n, x) \in \bigcap \Phi$.
          Then $(\succ(n), f(x)) \in \bigcap \Phi$.
          Hence $\succ(n) \in \Psi$.
          Indeed $f(x) \in A$.
        Qed.
      Qed.

      Let us show that for all $n \in \Nat$ and all $x, y \in A$ if
      $(n, x), (n, y) \in \bigcap \Phi$ then $x = y$. \\
      Proof.
        (a) Define $\Theta = \{ n \in \Nat \mid$ for all $x, y \in A$ if
        $(n, x), (n, y) \in \bigcap \Phi$ then $x = y \}$.

        (1) $\Theta$ contains $0$. \\
        Proof.
          Let us show that for all $x, y \in A$ if $(0, x), (0, y) \in
          \bigcap \Phi$ then $x = y$.
            Let $x, y \in A$.
            Assume $(0, x), (0, y) \in \bigcap \Phi$.

            Let us show that $x, y = a$.
              Assume $x \neq a$ or $y \neq a$.

              Case $x \neq a$.
                $(0,x), (0,a)$ are contained in every element of $\Phi$.
                Then $(0,x), (0,a) \in \bigcap \Phi$.
                Take $H = (\bigcap \Phi) \setminus \set{(0,x)}$.

                Let us show that $H \in \Phi$.
                  (1) $H \in \pow(\Nat \times A)$.

                  (2) $(0,a) \in H$.

                  (3) For all $n \in \Nat$ and all $b \in A$ if
                  $(n,b) \in H$ then $(\succ(n), f(b)) \in H$. \\
                  Proof.
                    Let $n \in \Nat$ and $b \in A$.
                    Assume $(n,b) \in H$.
                    Then $(\succ(n), f(b)) \in \bigcap \Phi$.
                    We have $(\succ(n), f(b)) \neq (0,x)$.
                    Hence $(\succ(n), f(b)) \in H$.
                  Qed.
                End.

                Then $(0,x)$ is not contained in every member of $\Phi$.
                Contradiction.
              End.

              Case $y \neq a$.
                $(0,y), (0,a)$ are contained in every element of $\Phi$.
                Then $(0,y), (0,a) \in \bigcap \Phi$.
                Take $H = (\bigcap \Phi) \setminus \set{(0,y)}$.

                Let us show that $H \in \Phi$.
                  (1) $H \in \pow(\Nat \times A)$.

                  (2) $(0,a) \in H$.

                  (3) For all $n \in \Nat$ and all $b \in A$ if
                  $(n,b) \in H$ then $(\succ(n), f(b)) \in H$. \\
                  Proof.
                    Let $n \in \Nat$ and $b \in A$.
                    Assume $(n,b) \in H$.
                    Then $(\succ(n), f(b)) \in \bigcap \Phi$.
                    We have $(\succ(n), f(b)) \neq (0,y)$.
                    Hence $(\succ(n), f(b)) \in H$.
                  Qed.
                End.

                Then $(0,y)$ is not contained in every member of $\Phi$.
                Contradiction.
              End.
            End.
          End.
        Qed.

        (2) For all $n \in \Theta$ we have $\succ(n) \in \Theta$. \\
        Proof.
          Let $n \in \Theta$.
          Then for all $x, y \in A$ if $(n, x), (n, y) \in \bigcap \Phi$ then
          $x = y$.
          Consider a $b \in A$ such that $(n,b) \in \bigcap \Phi$.
          Then $(\succ(n), f(b)) \in \bigcap \Phi$.

          Let us show that for all $x, y \in A$ if $(\succ(n), x),
          (\succ(n), y) \in \bigcap \Phi$ then $x = f(b) = y$.
            Let $x, y \in A$.
            Assume $(\succ(n), x), (\succ(n), y) \in \bigcap \Phi$.
            Suppose $x \neq f(b)$ or $y \neq f(b)$.

            Case $x \neq f(b)$.
              Take $H = (\bigcap \Phi) \setminus \set{(\succ(n),x)}$.

              (a) $H \in \pow(\Nat \times A)$.

              (b) $(0,a) \in H$.
              Indeed $(0,a) \in \bigcap \Phi$ and $(0,a) \notin
              \set{(\succ(n),x)}$.

              (c) For all $m \in \Nat$ and all $z \in A$ if $(m,z) \in H$
              then $(\succ(m),f(z)) \in H$. \\
              Proof.
                Let $m \in \Nat$ and $z \in A$.
                Assume $(m,z) \in H$.
                Then $(m,z) \in \bigcap \Phi$.
                Hence $(\succ(m),f(z)) \in \bigcap \Phi$.
                $(\succ(m),f(z)) \neq (\succ(n),x)$.
                Therefore $(\succ(m),f(z)) \in H$.
              Qed.

              Thus $H \in \Phi$.
              Therefore every element of $\bigcap \Phi$ is contained in $H$.
              Consequently $(\succ(n),x) \in H$.
              Contradiction.
            End.

            Case $y \neq f(b)$.
              Take a class $H$ such that $H = (\bigcap \Phi) \setminus
              \set{(\succ(n),y)}$.

              (a) $H \in \pow(\Nat \times A)$.

              (b) $(0,a) \in H$.
              Indeed $(0,a) \in \bigcap \Phi$ and $(0,a) \notin
              \set{(\succ(n),y)}$.

              (c) For all $m \in \Nat$ and all $z \in A$ if $(m,z) \in H$
              then $(\succ(m),f(z)) \in H$. \\
              Proof.
                Let $m \in \Nat$ and $z \in A$.
                Assume $(m,z) \in H$.
                Then $(m,z) \in \bigcap \Phi$.
                Hence $(\succ(m),f(z)) \in \bigcap \Phi$.
                $(\succ(m),f(z)) \neq (\succ(n),y)$.
                Therefore $(\succ(m),f(z)) \in H$.
              Qed.

              Thus $H \in \Phi$.
              Therefore every element of $\bigcap \Phi$ is contained in $H$.
              Consequently $(\succ(n),y) \in H$.
              Contradiction.
            End.

            Hence it is wrong that $x \neq f(b)$ or $y \neq f(b)$.
            Consequently $x = f(b) = y$.
          End.

          Therefore $\succ(n) \in \Theta$ (by a).
        Qed.
      Qed.

      Define $\varphi(n) =$ ``choose $x \in A$ such that $(n, x) \in
      \bigcap \Phi$ in $x$'' for $n \in \Nat$.

      (1) Then $\varphi$ is a map from $\Nat$ to $A$ and we have
      $\varphi(0) = a$.

      (2) For all $n \in \Nat$ we have $\varphi(\succ(n)) =
      f(\varphi(n))$. \\
      Proof.
        Let $n \in \Nat$.
        Take $x \in A$ such that $\varphi(n) = x$.
        Then $(n, x) \in \bigcap \Phi$.
        Hence $(\succ(n), f(\varphi(n))) = (\succ(n), f(x)) \in \bigcap \Phi$.
        Thus $\varphi(\succ(n)) = f(\varphi(n))$.
      Qed.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{ARITHMETIC_02_7510132520910848}
      Let $A$ be a set and $a \in A$ and $f : A \to A$.
      Let $\varphi, \varphi' : \Nat \to A$.
      Assume that $\varphi$ and $\varphi'$ are recursively defined by $a$ and
      $f$.
      Then $\varphi = \varphi'$.
    \end{proposition}
    \begin{proof}
      Define $\Phi = \{ n \in \Nat \mid \varphi(n) = \varphi'(n) \}$.

      (1) $\Phi$ contains $0$.
      Indeed $\varphi(0) = a = \varphi'(0)$.

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

      Thus $\Phi$ contains every natural number.
      Consequently $\varphi(n) = \varphi'(n)$ for each $n \in \Nat$.
    \end{proof}
  \end{forthel}
\end{document}
