半順序集合において 「x<y でない」と「x≧y である」は同じ意味でない、という話

発端はババさんのこちらの投稿で

<blockquote class="twitter-tweet"><p lang="ja" dir="ltr"><a href="https://twitter.com/hashtag/%E3%83%90%E3%83%90%E3%81%AE%E8%87%AA%E4%BD%9C%E5%95%8F%E9%A1%8C?src=hash&amp;ref_src=twsrc%5Etfw">#ババの自作問題</a> <br>騙されたら終わり。<br><br>解答やヒントなどはリプでもDMでも気軽にどうぞ。 <a href="https://t.co/OBgXZsgpkR">pic.twitter.com/OBgXZsgpkR</a></p>&mdash; ババ。 (@wIkmnGisuJPRGWf) <a href="https://twitter.com/wIkmnGisuJPRGWf/status/1177191991970426880?ref_src=twsrc%5Etfw">September 26, 2019</a></blockquote> <script async src="https://platform.twitter.com/widgets.js" charset="utf-8"></script>

私の回答は次のようなものです

> 複素数の順序の定義によるが、例えば「実数の通常の順序を含む最小の順序」を考えると、これは実数の世界では全順序だが複素数の世界では半順序となるため、表題のような読み替えが出来ない

※ ちなみに他の順序、例えば辞書式順序などを考えるとこれも実数の通常の順序を含みますが、全順序となるので表題の読み替えが可能となります。この場合は「 $x \geq -1 より x は実数であるため$ 」 という部分が誤りとなります。
※ 他の順序を入れたらどうなるかは未調査

この記事では全順序の場合に「 $x < y$ でない」 と 「$x \geq y$ である」 が同値であることの証明をしていきます。つまり命題は以下のようなものです：

関係 $\leq$ が全順序ならば、

```math
\lnot \bigl( x < y \bigr) \Longleftrightarrow x \geq y
```


直感で当たり前だと感じることの証明は結構難しかったりします。

# 定義

## 半順序

まず、半順序の定義を見ていきます。

集合 $P$ 上の半順序 $\leq$ とは、 $P$ 上の二項関係であって、下記を満たすものである：

```math
\begin{align}
反射律 && \forall x \in P,&&& x \leq x \\
反対称律 && \forall x, y \in P,&&& x \leq y \land y \leq x \Longrightarrow x = y \\
推移律 && \forall x, y, z \in P, &&& x \leq y \land y \leq z \Longrightarrow x \leq z
\end{align}
```

$P$ のことを関係 $\leq$ の台集合と言います。

## 全順序

次に、全順序とは以下のようなものです。

集合 $P$ 上の全順序 $\leq$ とは、 $\leq$ は$P$ 上の二項関係であって、下記を満たすものである：

```math
\begin{align}
反射律 && \forall x \in P,&&& x \leq x \\
反対称律 && \forall x, y \in P,&&& x \leq y \land y \leq x \Longrightarrow x = y \\
推移律 && \forall x, y, z \in P, &&& x \leq y \land y \leq z \Longrightarrow x \leq z \\
全順序律 && \forall x, y \in P, &&& x \leq y \lor y \leq x
\end{align}
```

半順序に加え、「全順序律」なるものが加わっています。これは $P$ の任意の元 $x$ と $y$ が比較可能、つまり $x \leq y$ または $y \leq x$ が必ず成り立つことを意味します。逆に半順序は比較不能な元が存在するかもしれません。全順序ならば半順序ですが、半順序であって全順序でないものも存在します。以下、全順序と半順序を総称して「順序」と呼びます。

## 全順序、半順序の具体例

整数や実数、有理数は通常の大小関係で順序が定義できます。この順序は全順序です。
ある集合の冪集合に対し、包含関係を順序として定義できます。この順序は半順序です。

実数の通常の順序を $\leq_{\mathbb{R}}$ と書くことにします。今、この順序を利用して複素数の順序 $\leq_{\mathbb{C}}$ を次のように定義します。

```math
\forall x, y \in \mathbb{C}, a \leq_{\mathbb{C}} b \overset{\text{def}}{\Longleftrightarrow} \bigl( a, b \in \mathbb{R} \land a \leq_{\mathbb{R}} b \bigr) \lor (a = b)
```

するとこれは反射律、反対称律、推移律を満たしています（証明略）。また、 $\text{i} \leq -\text{i}$ でも $-\text{i} \leq \text{i}$ でも無いので全順序律を満たしません。つまり $\leq_{\mathbb{C}}$ は半順序です。

## < の定義

$x < y $ を次のように定義します。

```math
x < y \overset{\text{def}}{\Longleftrightarrow} x \leq y \land x \neq y
```

## ≧ の定義

$x \geq y$ を次のように定義します。

```math
x \geq y \overset{\text{def}}{\Longleftrightarrow} y \leq x
```

# 証明

$\Longleftrightarrow$ を証明するために、 $\Longrightarrow$ と $\Longleftarrow$ を別々に見ていきます。
以下で、 $P$ を台集合、 $\leq$ を $P$ 上の全順序とします。

## →

まず $\lnot \bigl( x < y \bigr) \Longrightarrow x \geq y$ を示します。反射律から始まり、同値な変形を繰り返して導きます。

```math
\begin{align}
\forall x, y \in P, \\
&&& x = y \Longrightarrow y \leq x &&& \bigl( \because & 反射律 \bigr) \\
\Longleftrightarrow &&& x \neq y \lor y \leq x &&& \bigl( \because & \Rightarrow の定義 \bigr) \\
\Longleftrightarrow &&& \bigl( x \leq y \lor y \leq x \bigr) \land \bigl( x \neq y \lor y \leq x \bigr) &&& \bigl( \because & 全順序律より、x \leq y \lor y \leq x は恒真) \\
\Longleftrightarrow &&& \bigl( x \leq y \land x \neq y \bigr) \lor y \leq x &&& \bigl( \because & 因数分解) \\
\Longleftrightarrow &&& x < y \lor y \leq x &&& \bigl( \because & < の定義) \\
\Longleftrightarrow &&& \lnot \bigl( x < y \bigr) \Longrightarrow y \leq x &&& \bigl( \because & \Rightarrow の定義 \bigr) \\
\Longleftrightarrow &&& \lnot \bigl( x < y \bigr) \Longrightarrow x \geq y &&& \bigl( \because & \geq の定義 \bigr) \\
\end{align}
```

## ←
次に、 $\lnot \bigl( x < y \bigr) \Longleftarrow x \geq y$ を示します。 $\Longrightarrow$ 同様、同値変形を繰り返していきます。

```math
\begin{align}
\forall x, y \in P, \\
&&& x \leq y \land y \leq x \Longrightarrow x = y &&& \bigl( \because & 反対称律 \bigr) \\
\Longleftrightarrow &&& \lnot \bigl( x \leq y \land y \leq x \bigr) \lor x = y &&& \bigl( \because & \Rightarrow の定義 \bigr) \\
\Longleftrightarrow &&& \lnot \bigl( x \leq y \bigr) \lor \lnot \bigl( y \leq x \bigr) \lor x = y &&& \bigl( \because & \lnot の展開 \bigr) \\
\Longleftrightarrow &&& \lnot \bigl( y \leq x \bigr) \lor \lnot \bigl( x \leq y \bigr) \lor x = y &&& \bigl( \because & \lor の可換性 \bigr) \\
\Longleftrightarrow &&& \lnot \bigl( y \leq x \bigr) \lor \lnot \bigl( x \leq y \land x \neq y \bigr) &&& \bigl( \because & \lnot の因数分解 \bigr) \\
\Longleftrightarrow &&& \lnot \bigl( y \leq x \bigr) \lor \lnot \bigl( x < y \bigr) &&& \bigl( \because & < の定義 \bigr) \\
\Longleftrightarrow &&& y \leq x \Longrightarrow \lnot \bigl( x < y \bigr) &&& \bigl( \because & \Rightarrow の定義 \bigr) \\
\Longleftrightarrow &&& x \geq y \Longrightarrow \lnot \bigl( x < y \bigr) &&& \bigl( \because & \geq の定義 \bigr) \\
\end{align}
```

以上により、 「$x < y$ でない」 と 「$ x \geq y $」 が同値であることが言えました。

# 蛇足

証明をよく読むと、次のようなことがわかります。

-  全順序律を使っているのは 「x < y でない」 ならば 「x ≧ y である」 の場合のみ

つまり、 「x ≧ y である」 ならば 「x < y でない」 は、半順序集合でも成り立ちます。
例えば $ \text{i} \geq\_{\mathbb{C}} \text{i} $ ですが、 $ \text{i} = \text{i} $ ですので $ \text{i} <\_{\mathbb{C}} \text{i} $ ではありません。 $5 \geq\_{\mathbb{C}} 3$ ですが、 $5 <\_{\mathbb{C}} 3$ ではありません。

逆に、 $x <\_{\mathbb{C}} y$ でなく $ x \geq\_{\mathbb{C}} y$ でもない例として、 $1 + \text{i}$ と $1 - \text{i}$ などがあります。