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

\begin{document}
  \chapter{Binary relations}\label{chapter:binary-relations}

  \filename{foundations/sections/11_binary-relations.ftl.tex}

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

    [readtex \path{foundations/sections/10_sets.ftl.tex}]

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

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_6429308924985344}
      A binary relation is a class $R$ such that every element of $R$ is a pair.
    \end{definition}
  \end{forthel}


  \section{Properties of relations}

  \paragraph{Reflexivity}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_1126092393938944}
      Let $R$ be a binary relation and $A$ be a class.
      $R$ is reflexive on $A$ iff for all $a \in A$ we have $(a,a) \in R$.
    \end{definition}
  \end{forthel}


  \paragraph{Irreflexivity}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_365656446861312}
      Let $R$ be a binary relation and $A$ be a class.
      $R$ is irreflexive on $A$ iff for no $a \in A$ we have $(a,a) \in R$.
    \end{definition}
  \end{forthel}


  \paragraph{Symmetry}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_2056300137545728}
      Let $R$ be a binary relation and $A$ be a class.
      $R$ is symmetric on $A$ iff for all $a, b \in A$ if $(a,b) \in R$ then
      $(b,a) \in R$.
    \end{definition}
  \end{forthel}


  \paragraph{Antisymmetry}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_8301693043212288}
      Let $R$ be a binary relation and $A$ be a class.
      $R$ is antisymmetric on $A$ iff for all distinct $a, b \in A$ we have
      $(a,b) \notin R$ or $(b,a) \notin R$.
    \end{definition}
  \end{forthel}


  \paragraph{Asymmetry}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_6895428727472128}
      Let $R$ be a binary relation and $A$ be a class.
      $R$ is asymmetric on $A$ iff for all $a, b \in A$ if $(a,b) \in R$ then
      $(b,a) \notin R$.
    \end{definition}
  \end{forthel}


  \paragraph{Transitivity}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_5377309666181120}
      Let $R$ be a binary relation and $A$ be a class.
      $R$ is transitive on $A$ iff for all $a, b, c \in A$ if $(a,b) \in R$ and
      $(b,c) \in R$ then $(a,c) \in R$.
    \end{definition}
  \end{forthel}


  \paragraph{Connectedness}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_5902056743239680}
      Let $R$ be a binary relation and $A$ be a class.
      $R$ is connected on $A$ iff for all distinct $a, b \in A$ we have
      $(a,b) \in R$ or $(b,a) \in R$.
    \end{definition}
  \end{forthel}


  \paragraph{Strong connectedness}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_6492592562765824}
      Let $R$ be a binary relation and $A$ be a class.
      $R$ is strongly connected on $A$ iff for all $a, b \in A$ we have
      $(a,b) \in R$ or $(b,a) \in R$.
    \end{definition}
  \end{forthel}


  \section{Order relations}

  \paragraph{Preorders.}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_4005024520732672}
      Let $A$ be a class.
      A preorder on $A$ is a binary relation that is reflexive on $A$ and
      transitive on $A$.
    \end{definition}
  \end{forthel}


  \paragraph{Partial orders.}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_2162776243961856}
      Let $A$ be a class.
      A partial order on $A$ is a binary relation $R$ that is reflexive on $A$
      and antisymmetric on $A$ and transitive on $A$.
    \end{definition}

    Let $A$ is partially ordered by $R$ stand for $R$ is a partial order on $A$.
  \end{forthel}


  \paragraph{Strict partial orders.}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_4067384857985024}
      Let $A$ be a class.
      A strict preorder on $A$ is a binary relation that is irreflexive on $A$
      and transitive on $A$.
    \end{definition}

    Let $A$ is strictly preordered by $R$ stand for $R$ is a strict preorder
    on $A$.
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_11_5567849812721664}
      Let $A$ be a class.
      Any strict preorder on $A$ is antisymmetric on $A$.
    \end{proposition}

    Let a strict partial order on $A$ stand for a strict preorder on $A$.
    Let $A$ is strictly partially ordered by $R$ stand for $R$ is a strict
    partial order on $A$.
  \end{forthel}


  \paragraph{Total orders.}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_5872706501214208}
      Let $A$ be a class.
      A total order on $A$ is a partial order on $A$ that is connected on $A$.
    \end{definition}

    Let $A$ is totally ordered by $R$ stand for $R$ is a total order on $A$.

    Let a linear order on $A$ stand for a total order on $A$.
    Let $A$ is linearly ordered by $R$ stand for $R$ is a linear order on $A$.
  \end{forthel}


  \paragraph{Strict total orders.}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_5840248768561152}
      Let $A$ be a class.
      A strict total order on $A$ is a strict partial order on $A$ that is
      connected on $A$.
    \end{definition}

    Let $A$ is stritcly totally ordered by $R$ stand for $R$ is a strict total
    order on $A$.

    Let a strict linear order on $A$ stand for a strict total order on $A$.
    Let $A$ is strictly linearly ordered by $R$ stand for $R$ is a strict
    linear order on $A$.
  \end{forthel}


  \section{Well-founded relations}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_2729326472593408}
      Let $A$ be a class and $R$ be a binary relation.
      A least element of $A$ regarding $R$ is an element $a$ of $A$ such that
      there exists no $x \in A$ such that $(x,a) \in R$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_2420057567133696}
      Let $A$ be a class and $R$ be a binary relation.
      $R$ is wellfounded on $A$ iff every nonempty subclass of $A$ has a
      least element regarding $R$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_3262141912055808}
      Let $A$ be a class and $R$ be a binary relation.
      $R$ is strongly wellfounded on $A$ iff $R$ is wellfounded on $A$ and for
      all $b \in A$ there exists a set $X$ such that
      \[ X = \{ a \in A \mid (a,b) \in R \}. \]
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_6149137814781952}
      Let $A$ be a class.
      A wellorder on $A$ is a strict linear order on $A$ that is wellfounded on
      $A$.
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_8163723743068160}
      Let $A$ be a class.
      A strong wellorder on $A$ is a strict linear order on $A$ that is
      strongly wellfounded on $A$.
    \end{definition}
  \end{forthel}


  \section{Epsilon induction}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_11_4800525813940224}
      \[ {\in} = \{ (a,x) \mid \text{$x$ is a set that contains $a$} \}. \]
    \end{definition}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_11_5668859243659264}
      ${\in}$ is strongly wellfounded on any system of sets.
    \end{proposition}
    \begin{proof}
      Let $X$ be a system of sets.

      (1) ${\in}$ is wellfounded on $X$. \\
      Proof.
        Let $A$ be a nonempty subclass of $X$.
        Take an element $x$ of $A$ such that $A$ and $x$ are disjoint.
        Then $x$ is a least element of $A$ regarding ${\in}$.
        Indeed for any $a \in A$ if $a \in x$ then $a \in A \cap x$.
      Qed.

      (2) For all $x \in X$ there exists a set $Y$ such that
      $Y = \{ y \in X \mid (y,x) \in {\in} \}$. \\
      Proof.
        Let $x \in X$.
        Define $Y = \{ y \in X \mid (y,x) \in {\in} \}$.
        Then $Y = \{ y \in X \mid y \in x \}$.
        Hence $Y$ is a subclass of $x$.
        Thus $Y$ is a set.
      Qed.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{corollary}\printlabel{FOUNDATIONS_11_6337807438053376}
      Every nonempty system of sets has a least element regarding ${\in}$.
    \end{corollary}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_11_2812087589928960}
      Let $\Phi$ be a class.
      (Induction hypothesis) Assume that for all sets $x$ if $\Phi$ contains
      every element of $x$ that is a set then $\Phi$ contains $x$.
      Then $\Phi$ contains every set.
    \end{proposition}
    \begin{proof}
      Assume the contrary.
      Define $M = \{ x \mid x$ is a set such that $x \notin \Phi \}$.
      Then $M$ is nonempty.
      Hence we can take a least element $x$ of $M$ regarding ${\in}$.
      Then $x$ is a set such that every element of $x$ that is a set is
      contained in $\Phi$.
      Thus $\Phi$ contains $x$ (by induction hypothesis).
      Contradiction.
    \end{proof}
  \end{forthel}
\end{document}
