ていへんかけるたかさわるに

$S$ を任意の集合とし, $R \subset S \times S$ を $S$ 上の任意の関係とする.
このとき, $R$ を含む同値関係 $E$ で, $R$ を含む任意の同値関係 $E'$ に対して $E \subset E'$ を満たすものが一意的に存在する.
このような $E$ を, $R$ によって生成された $S$ 上の同値関係 と呼ぶ.

言い換えれば, $R$ を含む $S$ 上の同値関係全体の集合を $\mathrm{er}(R)$ とおいたとき, $R$ によって生成される一意的な同値関係 $E$ は
\begin{equation*}
\newcommand{\Ar}[1]{\mathrm{Ar}{#1}}
\newcommand{\ar}{\mathrm{ar}}
\newcommand{\arop}{\Opp{\mathrm{ar}}}
\newcommand{\Hom}{\mathrm{Hom}}
\newcommand{\Id}[1]{\mathrm{id}_{#1}}
\newcommand{\Mr}[1]{\mathrm{#1}}
\newcommand{\Ms}[1]{\mathscr{#1}}
\newcommand{\Ob}[1]{\mathrm{Ob}(#1)}
\newcommand{\Opp}[1]{{#1}^{\mathrm{op}}}
\newcommand{\Pos}{\mathbf{Pos}}
\newcommand{\q}{\hspace{1em}}
\newcommand{\qq}{\hspace{0.5em}}
\newcommand{Rest}[2]{{#1}|{#2}}
\newcommand{\Src}{d^{0,\mathrm{op}}}
\newcommand{\Tgt}{d^{1,\mathrm{op}}}
E = \bigcap_{E' \in \Mr{er}(R)} E'
\end{equation*} によって定まる.

この右辺:
\begin{equation*}
\bigcap_{E' \in \Mr{er}(R)} E'
\end{equation*} が $R$ を含む $S$ 上の同値関係として, 空集合 $\varnothing$ などにならずに定まることは自明ではないので証明が必要である.

$E$ は次のように構成する.

まず
\begin{equation*}
S_1 = S \times S, \quad S_2 = S \times S, \quad S_3 = S \times S \times S
\end{equation*}
とおき, 関数 $r : S_1 + S_2 + S_3 \to S \times S$ ($+$ は集合の非交和を表わす) を
\begin{align*}
\Rest{r}{S_1} &= (p_1, p_2) = \Id{S_1}, \\
\Rest{r}{S_2} &= (p_2, p_1), \\
\Rest{r}{S_3} &= (p_1, p_3)
\end{align*} と定義する.

次に $S$ の対角集合 $D$ を
\begin{equation*}
D = \left\{\, (x, x) \mid x \in S \,\right\}
\end{equation*} とおき,
\begin{align*}
E_0 &= D \cup R,\quad E_{0,1} = E_0 = E_{0,2}, \\
T_0 &= \left\{\, (x, y, z) \mid (x, y), (y, z) \in E_0 \,\right\}, \\
B_0 &= E_{0,1} + E_{0,2} + T_0
\end{align*} と定義する. ここで $B_0$ は $E_{0,1} = E_0$, $E_{0,2} = E_0$, $T_0$ の非交和である.

ある正の整数 $n$ に対して
\begin{align*}
& E_{n-1},\quad E_{n-1,1} = E_{n-1} = E_{n-1,2}, \\
& T_{n-1}, \\
& B_{n-1} = E_{n-1,1} + E_{n-1,2} + T_{n-1},
\end{align*} がそれぞれ定義されているとき, $E_n, T_n, B_n$ を
\begin{align*}
E_n &= r(B_{n-1}),\quad E_{n,1} = E_n = E_{n,2}, \\
T_n &= \left\{\, (x, y, z) \mid (x, y), (y, z) \in E_n \,\right\}, \\
B_n &= E_{n,1} + E_{n,2} + T_n,
\end{align*} のように定義する. これによって $S$ 上の $R$ を含む関係の列
\begin{equation*}
E_0, E_1,...
\end{equation*} が構成される.

このとき,
\begin{equation*}
E_n \subset E_{n+1} \quad (n = 0, 1,\ldots)
\end{equation*} が成り立つ.
$S$ 上の関係 $E$ を
\begin{equation*}
E = \bigcup_{n=0}^{\infty} E_n
\end{equation*} により定義する.

この $E$ が $R$ を含む $S$ 上の同値関係であって
\begin{equation*}
E = \bigcap_{E' \in \Mr{er}(R)} E'
\end{equation*} を満たすことがわかる. つまり $R$ によって一意的に生成される $S$ 上の同値関係となっている.

この構成は数学的帰納法によるもので, プログラミングをしているようだった.

証明がそれ自身プログラムのようなものになっている. 面白い.
※: 構成的プログラミングという理論がこのようなことを扱う分野だったと思うが詳しいことはわからない.