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

\begin{document}
  \chapter{Ordinal numbers}\label{chapter:ordinals}

  \filename{set-theory/sections/02_ordinals.ftl.tex}

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

    [readtex \path{foundations/sections/11_binary-relations.ftl.tex}]

    [readtex \path{set-theory/sections/01_transitive-classes.ftl.tex}]

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


  \begin{forthel}
    \begin{definition}\printlabel{SET_THEORY_02_229593678086144}
      An ordinal number is a transitive set $\alpha$ such that every element of
      $\alpha$ is a transitive set.
    \end{definition}

    Let an ordinal stand for an ordinal number.
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{SET_THEORY_02_5852994258075648}
      $\Ord$ is the class of all ordinals.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_02_2358097091756032}
      Let $\alpha$ be an ordinal.
      Then every element of $\alpha$ is an ordinal.
    \end{proposition}
    \begin{proof}
      Let $x$ be an element of $\alpha$.
      Then $x$ is transitive.

      Let us show that every element of $x$ is a subset of $x$.
        Let $y$ be an element of $x$.
        Then $y$ is a subset of $x$.
        Let $z$ be an element of $y$.
        Every element of $y$ is an element of $x$.
        Hence $z$ is an element of $x$.
      End.

      Thus every element of $x$ is transitive.
      Therefore $x$ is an ordinal.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_02_7202164443185152}
      Let $\alpha$ be an ordinal and $x \subseteq \alpha$.
      Then $\bigcup x$ is an ordinal.
    \end{proposition}
    \begin{proof}
      (1) $\bigcup x$ is transitive. \\
      Proof.
        Let $y \in \bigcup x$ and $z \in y$.
        Take $w \in x$ such that $y \in w$.
        Then $w \in \alpha$.
        Hence $w$ is transitive.
        Thus $z \in w$.
        Therefore $z \in \bigcup x$.
      Qed.

      (2) Every element of $\bigcup x$ is transitive. \\
      Proof.
        Let $y \in \bigcup x$.
        Let $z \in y$ and $v \in z$.
        Take $w \in x$ such that $y \in w$.
        We have $w \in \alpha$.
        Hence $w$ is an ordinal.
        Thus $y$ is an ordinal.
        Therefore $y$ is transitive.
        Consequently $v \in y$.
      Qed.
    \end{proof}
  \end{forthel}


  \section{Zero and successors}

  \begin{forthel}
    \begin{definition}\printlabel{SET_THEORY_02_8385964858671104}
      $0 = \emptyset$.
    \end{definition}

    Let $\alpha$ is nonzero stand for $\alpha \neq 0$.
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{SET_THEORY_02_8166925802668032}
      Let $\alpha$ be an ordinal.
      $\succ(\alpha) = \alpha \cup \set{\alpha}$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_02_8483196888940544}
      $0$ is an ordinal.
    \end{proposition}
    \begin{proof}
      Every element of $0$ is a transitive set and every element of $0$ is a
      subset of $0$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_02_1624410224066560}
      Let $\alpha$ be an ordinal.
      Then $\succ(\alpha)$ is an ordinal.
    \end{proposition}
    \begin{proof}
      (1) $\succ(\alpha)$ is transitive. \\
      Proof.
        Let $x \in \succ(\alpha)$ and $y \in x$.
        Then $x \in \alpha$ or $x = \alpha$.
        Hence $y \in \alpha$.
        Thus $y \in \succ(\alpha)$.
      Qed.

      (2) Every element of $\succ(\alpha)$ is transitive. \\
      Proof.
        Let $x \in \succ(\alpha)$.
        Then $x \in \alpha$ or $x = \alpha$.
        Hence $x$ is transitive.
        Indeed $\alpha$ is transitive and every element of $\alpha$ is
        transitive.
      Qed.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_02_8651096763400192}
      Let $\alpha, \beta$ be ordinals.
      If $\succ(\alpha) = \succ(\beta)$ then $\alpha = \beta$.
    \end{proposition}
    \begin{proof}
      Assume $\succ(\alpha) = \succ(\beta)$.

      (1) $\alpha \subseteq \beta$. \\
      Proof.
        Let $\gamma \in \alpha$.
        Then $\gamma \in \alpha \cup \set{\alpha}
          = \succ(\alpha)
          = \succ(\beta)
          = \beta \cup \set{\beta}$.
        Hence $\gamma \in \beta$ or $\gamma = \beta$.
        Assume $\gamma = \beta$.
        Then $\beta \in \alpha$.
        Hence $\beta
          = (\beta \cup \set{\beta}) \setminus \set{\gamma}
          = (\alpha \cup \set{\alpha}) \setminus \set{\gamma}
          = (\alpha \setminus \set{\gamma}) \cup \set{\alpha}$.
        Therefore $\alpha \in \beta$.
        Consequently $\alpha \in \beta \in \alpha$.
        Contradiction.
      Qed.

      (2) $\beta \subseteq \alpha$. \\
      Proof.
        Let $\gamma \in \beta$.
        Then $\gamma \in \beta \cup \set{\beta}
          = \succ(\beta)
          = \succ(\alpha)
          = \alpha \cup \set{\alpha}$.
        Hence $\gamma \in \alpha$ or $\gamma = \alpha$.
        Assume $\gamma = \alpha$.
        Then $\alpha \in \beta$.
        Hence $\alpha
          = (\alpha \cup \set{\alpha}) \setminus \set{\gamma}
          = (\beta \cup \set{\beta}) \setminus \set{\gamma}
          = (\beta \setminus \set{\gamma}) \cup \set{\beta}$.
        Therefore $\beta \in \alpha$.
        Consequently $\beta \in \alpha \in \beta$.
        Contradiction.
      Qed.
    \end{proof}
  \end{forthel}


  \section{The standard ordering of the ordinals}

  \begin{forthel}
    \begin{definition}\printlabel{SET_THEORY_02_6654252130762752}
      Let $\alpha, \beta$ be ordinals.
      $\alpha$ is less than $\beta$ iff $\alpha \in \beta$.
    \end{definition}

    Let $\alpha < \beta$ stand for $\alpha$ is less than $\beta$.
    Let $\alpha \nless \beta$ stand for not $\alpha < \beta$.

    Let $\alpha$ is greater than $\beta$ stand for $\beta < \alpha$.
    Let $\alpha > \beta$ stand for $\beta < \alpha$.
    Let $\alpha \ngtr \beta$ stand for not $\alpha > \beta$.
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{SET_THEORY_02_2639956210089984}
      Let $\alpha, \beta$ be ordinals.
      $\alpha$ is less than or equal to $\beta$ iff $\alpha < \beta$ or
      $\alpha = \beta$.
    \end{definition}

    Let $\alpha \leq \beta$ stand for $\alpha$ is less than or equal to $\beta$.
    Let $\alpha \nleq \beta$ stand for not $\alpha \leq \beta$.

    Let $\alpha$ is greater than or equal to $\beta$ stand for
    $\beta \leq \alpha$.
    Let $\alpha \geq \beta$ stand for $\beta \leq \alpha$.
    Let $\alpha \ngeq \beta$ stand for not $\alpha \geq \beta$.
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_02_3089369577553920}
      Let $\alpha, \beta$ be ordinals.
      Then \[ \alpha \leq \beta \implies \alpha \subseteq \beta. \]
    \end{proposition}
    \begin{proof}
      Case $\alpha \leq \beta$.
        Then $\alpha < \beta$ or $\alpha = \beta$.
        Let $x \in \alpha$.
        If $\alpha < \beta$ then $x \in \alpha \in \beta$.
        Hence if $\alpha < \beta$ then $x \in \beta$.
        If $\alpha = \beta$ then $x \in \beta$.
        Thus $x \in \beta$.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_02_6229364135952384}
      Let $\alpha$ be an ordinal.
      Then \[ \alpha \nless \alpha. \]
    \end{proposition}
    \begin{proof}
      Assume $\alpha < \alpha$.
      Then $\alpha \in \alpha$.
      Contradiction.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_02_7098683017396224}
      Let $\alpha, \beta, \gamma$ be ordinals.
      Then \[ (\text{$\alpha < \beta$ and $\beta < \gamma$}) \implies
      \alpha < \gamma. \]
    \end{proposition}
    \begin{proof}
      Assume $\alpha < \beta$ and $\beta < \gamma$.
      Then $\alpha \in \beta \in \gamma$.
      Hence $\alpha \in \gamma$.
      Thus $\alpha < \gamma$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_02_1718825707896832}
      Let $\alpha, \beta$ be ordinals.
      Then $\alpha < \beta$ or $\alpha = \beta$ or $\alpha > \beta$.
    \end{proposition}
    \begin{proof}
      Assume the contrary.
      Define \[ A = \class{\alpha' \in \Ord | \classtext{there exists an ordinal
      $\beta'$ such that neither $\alpha' < \beta'$ nor $\alpha' = \beta'$ nor
      $\alpha' > \beta'$}}. \]
      $A$ is nonempty.
      Hence we can take a least element $\alpha'$ of $A$ regarding ${\in}$.
      Define \[ B = \{ \beta' \in \Ord \mid \text{neither $\alpha' < \beta'$
      nor $\alpha' = \beta'$ nor $\alpha' > \beta'$} \}. \]
      $B$ is nonempty.
      Hence we can take a least element $\beta'$ of $B$ regarding ${\in}$.

      Let us show that $\alpha' \subseteq \beta'$.
        Let $a \in \alpha'$.
        Then $a < \beta'$ or $a = \beta'$ or $a > \beta'$.
        Indeed if neither $a < \beta'$ nor $a = \beta'$ nor $a > \beta'$ then
        $a \in A$.
        If $a = \beta'$ then $\beta' < \alpha'$.
        If $a > \beta'$ then $\beta' < \alpha'$.
        Hence $a < \beta'$.
        Thus $a \in \beta'$.
      End.

      Let us show that $\beta' \subseteq \alpha'$.
        Let $b \in \beta'$.
        Then $b < \alpha'$ or $b = \alpha'$ or $b > \alpha'$.
        If $b = \alpha'$ then $\alpha' < \beta'$.
        If $b > \alpha'$ then $\alpha' < \beta'$.
        Hence $b < \alpha'$.
        Thus $b \in \alpha'$.
      End.

      Hence $\alpha' = \beta'$.
      Contradiction.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_02_610496856195072}
      Let $\alpha, \beta$ be ordinals.
      Then \[ \alpha \subseteq \beta \implies \alpha \leq \beta. \]
    \end{proposition}
    \begin{proof}
      Assume $\alpha \subseteq \beta$.

      Case $\alpha = \beta$. Trivial.

      Case $\alpha \neq \beta$.
        Then $\alpha < \beta$ or $\alpha > \beta$.
        Assume $\alpha > \beta$.
        Then $\beta \in \alpha$.
        Hence $\beta \in \beta$.
        Contradiction.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_02_5689190964527104}
      Let $\alpha$ be an ordinal.
      Then \[ \alpha < \succ(\alpha). \]
    \end{proposition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_02_4064972025888768}
      Let $\alpha, \beta$ be ordinals.
      Then \[ \beta < \succ(\alpha) \implies \beta \leq \alpha. \]
    \end{proposition}
    \begin{proof}
      Assume $\beta < \succ(\alpha)$.
      Then $\beta \in \succ(\alpha) = \alpha \cup \set{\alpha}$.
      Hence $\beta \in \alpha$ or $\beta \in \set{\alpha}$.
      Thus $\beta < \alpha$ or $\beta = \alpha$.
      Therefore $\beta \leq \alpha$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_02_8242798790705152}
      Let $\alpha$ be an ordinal.
      There exists no ordinal $\beta$ such that
      $\alpha < \beta < \succ(\alpha)$.
    \end{proposition}
    \begin{proof}
      Assume the contrary.
      Consider an ordinal $\beta$ such that $\alpha < \beta < \succ(\alpha)$.
      Then $\beta < \alpha$ or $\beta = \alpha$.
      Hence $\alpha < \alpha$.
      Contradiction.
    \end{proof}
  \end{forthel}


  \section{Successor and limit ordinals}

  \begin{forthel}
    \begin{definition}\printlabel{SET_THEORY_02_7129712109289472}
      A successor ordinal is an ordinal $\alpha$ such that
      $\alpha = \succ(\beta)$ for some ordinal $\beta$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_02_4240355610329088}
      Let $\alpha$ be an ordinal.
      There exists no ordinal $\beta$ such that
      $\alpha < \beta < \succ(\alpha)$.
    \end{proposition}
    \begin{proof}
      Assume the contrary.
      Choose an ordinal $\beta$ such that $\alpha < \beta < \succ(\alpha)$.
      Then $\alpha \in \beta \in \alpha \cup \set{\alpha}$.
      Hence $\beta \in \alpha$ or $\beta = \alpha$.
      Then $\alpha \in \alpha$.
      Contradiction.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{SET_THEORY_02_735071524880384}
      Let $\alpha$ be a successor ordinal.
      $\pred(\alpha)$ is the ordinal $\beta$ such that $\alpha = \succ(\beta)$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{SET_THEORY_02_7678388934279168}
      A limit ordinal is an ordinal $\lambda$ such that neither $\lambda$ is
      a successor ordinal nor $\lambda = 0$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_02_4659024620421120}
      Let $\lambda$ be a limit ordinal and $\alpha \in \lambda$.
      Then $\lambda$ contains $\succ(\alpha)$.
    \end{proposition}
    \begin{proof}
      If $\succ(\alpha) \notin \lambda$ then $\alpha < \lambda < \succ(\alpha)$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{theorem}[Burali-Forti]\printlabel{SET_THEORY_03_2217148434874368}
      $\Ord$ is a proper class.
    \end{theorem}
    \begin{proof}
      Assume that $\Ord$ is a set.
      $\Ord$ is transitive and every element of $\Ord$ is transitive.
      Hence $\Ord$ is an ordinal.
      Thus $\Ord \in \Ord$.
      Contradiction.
    \end{proof}
  \end{forthel}


  \section{Transfinite induction}

  \begin{forthel}
    \begin{definition}\printlabel{SET_THEORY_02_4059354166722560}
      \[ {<} = \{ (\alpha, \beta) \mid \text{$\alpha$ and $\beta$ are ordinals
      such that $\alpha < \beta$} \}. \]
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_02_4859038791630848}
      ${<}$ is a strong wellorder on $\Ord$.
    \end{proposition}
    \begin{proof}
      For any ordinals $\alpha, \beta$ we have $(\alpha,\beta) \in {<}$ iff
      $\alpha < \beta$.

      (1) ${<}$ is irreflexive on $\Ord$.
      Indeed for any ordinal $\alpha$ we have $\alpha \nless \alpha$.

      (2) ${<}$ is transitive on $\Ord$.
      Indeed for any ordinals $\alpha, \beta, \gamma$ if $\alpha < \beta$ and
      $\beta < \gamma$ then $\alpha < \gamma$.

      (3) ${<}$ is connected on $\Ord$.
      Indeed for any distinct ordinals $\alpha, \beta$ we have $\alpha < \beta$
      or $\beta < \alpha$.

      Hence ${<}$ is a strict linear order on $\Ord$.

      (4) ${<}$ is wellfounded on $\Ord$. \\
      Proof.
        Let $A$ be a nonempty subclass of $\Ord$.
        Then we can take a least element $\alpha$ of $A$ regarding ${\in}$.
        Then $\alpha$ is a least element of $A$ regarding ${<}$.
      Qed.

      Hence ${<}$ is strongly wellfounded on $\Ord$.
      Indeed for any $\beta \in \Ord$ we have $\beta = \{ \alpha \in \Ord \mid
      (\alpha,\beta) \in {<} \}$.
      Thus ${<}$ is a strong wellorder on $\Ord$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{corollary}\printlabel{SET_THEORY_02_1042046129274880}
      Let $A$ be a subclass of $\Ord$.
      If $A$ is nonempty then $A$ has a least element regarding ${<}$.
    \end{corollary}
  \end{forthel}

  \begin{forthel}
    \begin{corollary}\printlabel{SET_THEORY_02_1991423647809536}
      Let $A$ be a subclass of $\Ord$.
      If $A$ is nonempty then $A$ has a least element regarding ${\in}$.
    \end{corollary}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{SET_THEORY_03_8114657499807744}
      ${<}$ is a strong wellorder on any ordinal.
    \end{proposition}
    \begin{proof}
      Let $\alpha$ be an ordinal.
      For all $\beta, \gamma \in \alpha$ we have $(\beta,\gamma) \in {<}$ iff
      $\beta < \gamma$.

      (1) ${<}$ is irreflexive on $\alpha$.
      Indeed for all $\beta \in \alpha$ we have $\alpha \nless \alpha$.

      (2) ${<}$ is transitive on $\alpha$.
      Indeed for all $\beta, \gamma, \delta \in \alpha$ if $\beta < \gamma$ and
      $\gamma < \delta$ then $\beta < \delta$.

      (3) ${<}$ is connected on $\alpha$.
      Indeed for any distinct $\beta, \gamma \in \alpha$ we have
      $\beta < \gamma$ or $\gamma < \beta$.

      Hence ${<}$ is a strict linear order on $\alpha$.

      (4) ${<}$ is wellfounded on $\alpha$. \\
      Proof.
        Let $A$ be a nonempty subclass of $\alpha$.
        Then we can take a least element $\beta$ of $A$ regarding ${<}$.
        Indeed $A$ is a subclass of $\Ord$.
      Qed.

      Hence ${<}$ is strongly wellfounded on $\alpha$.
      Indeed for any $\gamma \in \alpha$ we have
      $\gamma = \{ \beta \in \Ord \mid (\beta,\gamma) \in {<} \}$.
      Thus ${<}$ is a strong wellorder on $\alpha$.
      [unfold off]
    \end{proof}
  \end{forthel}

  \noindent \textbf{Note:} In the proof below
  \ref{FOUNDATIONS_11_2812087589928960} refers to the Foundations library!

  \begin{forthel}
    \begin{theorem}\printlabel{SET_THEORY_02_8493935460614144}
      Let $\Phi$ be a class.
      Assume that for all ordinals $\alpha$ if $\Phi$ contains all ordinals
      less than $\alpha$ then $\Phi$ contains $\alpha$.
      Then $\Phi$ contains every ordinal.
    \end{theorem}
    \begin{proof}
      Define $B = \{ x \mid x$ is a set and if $x \in \Ord$ then
      $x \in \Phi \}$.

      Let us show that for all sets $x$ if $B$ contains every element of $x$
      that is a set then $B$ contains $x$.
        Let $x$ be a set.
        Assume that every element of $x$ that is a set is contained in $B$.

        Case $x \notin \Ord$. Trivial.

        Case $x \in \Ord$.
          Then $\Phi$ contains all ordinals less than $x$.
          Hence $\Phi$ contains $x$.
          Thus $x \in B$.
        End.
      End.

      [prover vampire]
      Hence $B$ contains every set (by \ref{FOUNDATIONS_11_2812087589928960}).
      Thus $\Phi$ contains every ordinal.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{theorem}\printlabel{SET_THEORY_02_7892040431960064}
      Let $\Phi$ be a class.
      (Initial case) Assume that $\Phi$ contains $0$.
      (Successor step) Assume that for all ordinals $\alpha$ if
      $\alpha \in \Phi$ then $\succ(\alpha) \in \Phi$.
      (Limit step) Assume that for all limit ordinals $\lambda$ if every
      ordinals less than $\lambda$ is contained in $\Phi$ then
      $\lambda \in \Phi$.
      Then $\Phi$ contains every ordinal.
    \end{theorem}
    \begin{proof}
      Let us show that for all ordinals $\alpha$ if $\Phi$ contains all ordinals
      less than $\alpha$ then $\Phi$ contains $\alpha$.
        Let $\alpha$ be an ordinal.
        Then $\alpha = 0$ or $\alpha$ is a successor ordinal or $\alpha$ is a
        limit ordinal.
        Assume that $\Phi$ contains all ordinals less than $\alpha$.

        Case $\alpha = 0$. Trivial.

        Case $\alpha$ is a successor ordinal.
          Take an ordinal $\beta$ such that $\alpha = \succ(\beta)$.
          Then $\beta \in \Phi$.
          Hence $\alpha \in \Phi$ (by successor step).
        End.

        Case $\alpha$ is a limit ordinal.
          Then $\beta \in \Phi$ for all ordinals $\beta$ less than $\alpha$.
          Hence $\alpha \in \Phi$ (by limit step).
        End.
      End.

      [prover vampire]
      Thus $\Phi$ contains every ordinal (by
      \ref{SET_THEORY_02_8493935460614144}).
    \end{proof}
  \end{forthel}
\end{document}
