MarriageTheoremのこと

某氏のサイト*1で日記を読んでいたら、以下のような命題とその証明が紹介してあった。まず用語をいくつか定義すると、半順序集合 \(\langle A,\leq_A \rangle\) の部分集合 \(S\) の（ \(A\) における）上界で \(S\) に属さないものが存在するとき、 \(A\) は強い意味で上に有界であると定める。また、 \(S \subset A\) が条件 \(\forall x,y \in A [x \in S \land y \leq_A x \rightarrow y \in S]\) を満たすとき、 \(S\) は下向きに閉じていると定める。さらに、 \(x \in A\) を切り口とする切片とは、部分集合 \(\mathrm{seg}_A(x) \colon= \{y \in A \colon y <_A x\}\) のことと定める。
件の命題は以下の通りである。

定理：全順序集合 \(\langle A,\leq_A \rangle\) の強い意味で上に有界で下向きに閉じた集合がすべてある要素を切り口とする切片であるなら、この全順序集合は整列集合である。

で、件の日記にはこの命題の証明も載っていたのだけど、（私の勘違いでなければ）ある部分集合における最小元の非存在から無限降下列の存在を導く際に従属選択公理（DC）が用いられているような気がして、本当にDCが必要なのかなぁと考えているうち、DCを使わない（と思われる）証明に気が付いた。といっても本質的にはもとの証明と同じことしかしていないのだが、MathJaxで数式を書く練習も兼ねてDCを使わない（と思われる）証明を記してみることにする。（なお、折角なので背理法も使わない*2ように注意してみた。）以下証明。
<証明> \(A\) の空でない部分集合 \(B\) が常に \(\leq_A\) -最小元を持つことを示す。 \(B\) が1元集合であれば自明なのでそうでない場合を考える。このとき、 \(B\) の \(\leq_A\) -最小元ではない元 \(b \in B\) が存在する。さて、 \(A\) における \(B\) の下界全体の集合を \(S\) とおくと、 \(S\) は下向きに閉じており、また \(b\) は選び方より \(S\) に属さない \(S\) の上界である。つまり \(S\) は強い意味で上に有界でもある。すると定理の仮定から、ある \(a \in A\) について \(S = \mathrm{seg}_A(a)\) が成り立つ。このとき \(a \not\in \mathrm{seg}_A(a) = S\) なので \(a\) は \(B\) の下界ではなく、 \(a \nleq_A b'\) となる \(b' \in B\) が存在する。 \(\leq_A\) は全順序なので \(b' <_A a\) 、従って \(b' \in \mathrm{seg}_A(a) = S\) であり、 \(S\) の定義から \(b'\) は \(B\) の下界であるが、一方で \(b'\) は \(B\) の元でもある。よって \(b'\) は \(B\) の \(\leq_A\) -最小元である。</証明>
（10/18追記）上記証明の論法を把握しやすくするために具体例を挙げておく。 \(A = \omega = \{0,1,2,\dots\}, B = (\mbox{奇数全体}) = \{1,3,5,\dots\}\) とし、 \(A\) の順序は普通の大小関係で定める。 \(b \in B\) は \(1\) 以外の \(B\) の元、例えば \(b = 3\) となる。 \(A\) における \(B\) の下界は \(0\) と \(1\) なので \(S = \{0,1\}\) となり、 \(a = 2 \in A\) について \(S = \mathrm{seg}_A(a)\) が成り立つ。（ \(B\) の最小元である \(1\) が \(S\) に属していることに注意されたい。）そして \(a \nleq b'\) となる（唯一の） \(b' \in B\) としては \(b' = 1\) が取れて、これは確かに \(B\) の最小元となっている。

_ ちなみに風邪の具合はどうなったかというと、↑こういうことを書ける程度には元気だけれども懇親会を休んでまで早くホテルに戻ってくる程度には元気じゃないみたい。

_ ↑↑の件で日記の主に確認したところ、DCを使わない証明も考えたけれども、その日が「選択公理の日」だったので（あと説明の簡略化のために）わざとDCを使用したとのこと。横綱相撲であるなぁ。