\documentclass[../../set-theory/set-theory.tex]{subfiles}

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

  \filename{set-theory/sections/04_recursion.ftl.tex}

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

    [readtex \path{set-theory/sections/02_ordinals.ftl.tex}]

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


  \begin{forthel}
    \begin{definition}\printlabel{SET_THEORY_04_7107446027845632}
      Let $A$ be a class and $\alpha$ be an ordinal.
      \[ A^{< \alpha} = \{ f \mid \text{$f$ is a map from $\beta$ to $A$
      for some ordinal $\beta$ less than $\alpha$} \}. \]
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{SET_THEORY_04_1955917673267200}
      Let $A$ be a class.
      \[ A^{< \infty} = \{f \mid \text{$f$ is a map from $\alpha$ to $A$
      for some ordinal $\alpha$} \}. \]
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{lemma}\printlabel{SET_THEORY_04_7841726894964736}
      Let $A$ be a class and $f$ be a map to $A$ such that $\dom(f)$ is a
      transitive subclass of $\Ord$ and $\alpha \in \dom(f)$.
      Then $f \restriction \alpha \in A^{< \infty}$.
    \end{lemma}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{SET_THEORY_04_5597213870784512}
      Let $H$ be a map and $G : A^{< \infty} \to A$ for some class $A$ such
      that $H$ is a map to $A$.
      $H$ is recursive regarding $G$ iff $\dom(H)$ is a transitive subclass of
      $\Ord$ and for all $\alpha \in \dom(H)$ we have
      \[ H(\alpha) = G(H \restriction \alpha). \]
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_04_2876133366300672}
      Let $A$ be a class and $G$ be a map from $A^{< \infty}$ to $A$.
      Let $H, H'$ be maps to $A$ that are recursive regarding $G$.
      Then \[ H(\alpha) = H'(\alpha) \]
      for all $\alpha \in \dom(H) \cap \dom(H')$.
    \end{proposition}
    \begin{proof}
      Define $\Phi = \{ \alpha \in \Ord \mid$ if
      $\alpha \in \dom(H) \cap \dom(H')$ then $H(\alpha) = H'(\alpha) \}$.

      For all ordinals $\alpha$ if every ordinal less than $\alpha$ lies in
      $\Phi$ then $\alpha \in \Phi$. \\
      Proof.
        Let $\alpha \in \Ord$.
        Assume that every $y \in \alpha$ lies in $\Phi$.

        Let us show that if $\alpha \in \dom(H) \cap \dom(H')$ then
        $H(\alpha) = H'(\alpha)$.
          Suppose $\alpha \in \dom(H) \cap \dom(H')$.
          Then $\alpha \subseteq \dom(H), \dom(H')$.
          Indeed $\dom(H)$ and $\dom(H')$ are transitive classes.
          Hence for all $y \in \alpha$ we have $y \in \dom(H) \cap \dom(H')$.
          Thus $H(y) = H'(y)$ for all $y \in \alpha$.
          Therefore $H \restriction \alpha = H' \restriction \alpha$.
          $H$ and $H'$ are recursive regarding $G$.
          Hence $H(\alpha)
            = G(H \restriction \alpha)
            = G(H' \restriction \alpha)
            = H'(\alpha)$.
        End.

        Thus $\alpha \in \Phi$.
      Qed.

      [prover vampire]
      Then $\Phi$ contains every ordinal (by
      \cref{SET_THEORY_02_8493935460614144}).
      Therefore we have $H(\alpha) = H'(\alpha)$ for all
      $\alpha \in \dom(H) \cap \dom(H')$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{theorem}[Recursion theorem]\printlabel{SET_THEORY_04_3600210873810944}
      Let $A$ be a class and $G$ be a map from $A^{< \infty}$ to $A$.
      Then there exists a map $F$ from $\Ord$ to $A$ that is recursive
      regarding $G$.
    \end{theorem}
    \begin{proof}
      Every ordinal is contained in the domain of some map $H$ to $A$ such that
      $H$ is recursive regarding $G$. \\
      Proof.
        Define \[ \Phi = \class{\alpha \in \Ord | \classtext{$\alpha$ is
        contained in the domain of some map to $A$ that is recursive regarding
        $G$}}. \]

        Let us show that for every ordinal $\alpha$ if every ordinal less than
        $\alpha$ lies in $\Phi$ then $\alpha \in \Phi$.
          Let $\alpha$ be an ordinal.
          Assume that every ordinal less than $\alpha$ lies in $\Phi$.
          Then for all $y \in \alpha$ there exists a map $h$ to $A$ such that
          $h$ is recursive regarding $G$ and $y \in \dom(h)$.
          Define $H'(y) =$ ``choose a map $h$ to $A$ such that $h$ is recursive
          regarding $G$ and $y \in \dom(h)$ in $h(y)$'' for $y \in \alpha$.
          Then $H'$ is a map from $\alpha$ to $A$.
          We have $H' = H' \restriction \alpha$.
          Define \[ H(\beta) =
            \begin{cases}
              H'(\beta)                 & : \beta < \alpha \\
              G(H' \restriction \beta)  & : \beta = \alpha
            \end{cases} \]
          for $\beta \in \succ(\alpha)$.
          Then $H \restriction \beta \in A^{< \infty}$ for all $\beta \in
          \dom(H)$.

          (a) $\dom(H)$ is a transitive subclass of $\Ord$.

          (b) For all $\beta \in \dom(H)$ we have $H(\beta) =
          G(H \restriction \beta)$. \\
          Proof.
            Let $\beta \in \dom(H)$.
            Then $\beta < \alpha$ or $\beta = \alpha$.

            Case $\beta < \alpha$.
              Choose a map $h$ to $A$ such that $h$ is recursive regarding $G$
              and $\beta \in \dom(h)$ and $H'(\beta) = h(\beta)$.

              Let us show that for all $y \in \beta$ we have $h(y) = H(y)$.
                Let $y \in \beta$.
                Then $H(y) = H'(y)$.
                Choose a map $h'$ to $A$ such that $h'$ is recursive regarding
                $G$ and $y \in \dom(h')$ and $H'(y) = h'(y)$.
                [prover vampire]
                Then $h'(y) = h(y)$ (by \cref{SET_THEORY_04_2876133366300672}).
                Indeed $y \in \dom(h) \cap \dom(h')$.
              End.

              Hence $h \restriction \beta = H \restriction \beta$.
              Thus $H(\beta)
                = H'(\beta)
                = h(\beta)
                = G(h \restriction \beta)
                = G(H \restriction \beta)$.
            End.

            Case $\beta = \alpha$.
              We have $H \restriction \alpha = H' \restriction \alpha$.
            End.
          Qed.

          Hence $H$ is a map to $A$ such that $H$ is recursive regarding $G$ and
          $\alpha \in \dom(H)$.
          Thus $\alpha \in \Phi$.
        End.

        [prover vampire]
        Therefore $\Phi$ contains every ordinal (by
        \cref{SET_THEORY_02_8493935460614144}).
        Consequently every ordinal is contained in the domain of some map $H$ to
        $A$ such that $H$ is recursive regarding $G$.
      Qed.

      Define $F(\alpha) =$ ``choose a map $H$ to $A$ such that $H$ is recursive
      regarding $G$ and $\alpha \in \dom(H)$ in $H(\alpha)$'' for
      $\alpha \in \Ord$.
      Then $F$ is a map from $\Ord$ to $A$.

      $F$ is recursive regarding $G$. \\
      Proof.
        (a) $\dom(F)$ is a transitive subclass of $\Ord$.

        (b) For all $\alpha \in \Ord$ we have $F(\alpha) =
        G(F \restriction \alpha)$. \\
        Proof.
          Let $\alpha \in \Ord$.
          Choose a map $H$ to $A$ such that $H$ is recursive regarding $G$ and
          $\alpha \in \dom(H)$ and $F(\alpha) = H(\alpha)$.

          Let us show that $F(\beta) = H(\beta)$ for all $\beta \in \alpha$.
            Let $\beta \in \alpha$.
            Choose a map $H'$ to $A$ such that $H'$ is recursive regarding $G$
            and $\beta \in \dom(H')$ and $F(\beta) = H'(\beta)$.
            [prover vampire]
            Then $H(\beta) = H'(\beta)$ (by
            \cref{SET_THEORY_04_2876133366300672}).
            Indeed $\beta \in \dom(H) \cap \dom(H')$.
            Therefore $F(\beta) = H'(\beta)$.
          End.

          Hence $H \restriction \alpha = F \restriction \alpha$.
          Thus $F(\alpha)
            = H(\alpha)
            = G(H \restriction \alpha)
            = G(F \restriction \alpha)$.
        Qed.
      Qed.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{theorem}\printlabel{SET_THEORY_04_1787371569807360}
      Let $A$ be a class and $G$ be a map from $A^{< \infty}$ to $A$.
      Let $F, F'$ be maps from $\Ord$ to $A$ that are recursive regarding $G$.
      Then $F = F'$.
    \end{theorem}
    \begin{proof}
      $F$ and $F'$ are recursive regarding $G$.
      [prover vampire]
      Then $F(\alpha) = F'(\alpha)$ for all $\alpha \in \dom(F) \cap \dom(F')$
      (by \cref{SET_THEORY_04_2876133366300672}).
      Indeed let $\alpha \in \dom(F) \cap \dom(F')$. % Looks redundant but the prover needs this step...
      We have $\dom(F) = \Ord = \dom(F')$.
      Hence $F(\alpha) = F'(\alpha)$ for all $\alpha \in \Ord$.
      Thus $F = F'$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{theorem}\printlabel{SET_THEORY_04_8446954438656000}
      Let $A$ be a class.
      Let $a \in A$ and $G : \Ord \times A \to A$ and
      $H : \Ord \times A^{< \infty} \to A$.
      Then there exists a map $F$ from $\Ord$ to $A$ such that
      \[ F(0) = a \]
      and for all ordinals $\alpha$ we have
      \[ F(\succ(\alpha)) = G(\alpha, F(\alpha)) \]
      and for all limit ordinals $\lambda$ we have
      \[ F(\lambda) = H(\lambda, F \restriction \lambda). \]
    \end{theorem}
    \begin{proof}
      Define  \[ J(f) =
        \begin{cases}
          a
          & : \dom(f) = 0
          \\
          G(\pred(\dom(f)), f(\pred(\dom(f))))
          & : \text{$\dom(f)$ is a successor ordinal}
          \\
          H(\dom(f), f)
          & : \text{$\dom(f)$ is a limit ordinal}
        \end{cases} \]
      for $f \in A^{< \infty}$.

      Then $J$ is a map from $A^{< \infty}$ to $A$.
      Indeed we can show that for any $f \in A^{< \infty}$ we have $J(f) \in A$.
        Let $f \in A^{< \infty}$.
        Take $\alpha \in \Ord$ such that $f : \alpha \to A$.
        If $\alpha = 0$ then $J(f) = a \in A$.
        If $\alpha$ is a successor ordinal then $J(f) =
        G(\pred(\alpha), f(\pred(\alpha))) \in A$.
        If $\alpha$ is a limit ordinal then $J(f) = H(\alpha, f) \in A$.
      End.

      Hence we can take a map $F$ from $\Ord$ to $A$ that is recursive regarding
      $J$.
      Then $F \restriction \alpha \in A^{< \infty}$ for any ordinal $\alpha$.

      (1) $F(0) = a$. \\
      Proof.
        $F(0)
          = J(F \restriction 0)
          = a$.
      Qed.

      (2) $F(\succ(\alpha)) = G(\alpha, F(\alpha))$ for all ordinals
      $\alpha$. \\
      Proof.
        Let $\alpha$ be an ordinal.
        Then $F(\succ(\alpha))
          = J(F \restriction \succ(\alpha))
          = G(\pred(\succ(\alpha)), (F \restriction \succ(\alpha))(\pred(\succ(\alpha))))
          = G(\alpha, (F \restriction \succ(\alpha))(\alpha))
          = G(\alpha, F(\alpha))$.
      Qed.

      (3) $F(\lambda) = H(\lambda, F \restriction \lambda)$ for all limit
      ordinals $\lambda$. \\
      Proof.
        Let $\lambda$ be a limit ordinal.
        Then $F(\lambda)
          = J(F \restriction \lambda)
          = H(\lambda, F \restriction \lambda)$.
      Qed.
    \end{proof}
  \end{forthel}
\end{document}
