エレファント・コンピューティング調査報告

極限に関する順序を論理プログラミングの手法を使って指定することを目指すブロクです。

エレファントな整数論(23)

写像の分類の説明

 M を集合、 s: M \to M写像とします。 \bar{s}: \mathfrak{P}(M) \to \mathfrak{P}(M) \mathcal{R}_x s^*: M \to \mathfrak{P}(M) を前回と同じものとします。 x_0 \in M をとり  N = s^*(x_0) とおきます。前回の説明を続けていきます。

 x \in N に対して

  •  N_{\le x} = \{ y \in N \mid y \le x \}
  •  N_{\cong x} = \{ y \in N \mid y \le x \ かつ \ x \le y \}

とおきます。

以下の条件を考えます。条件  (N_6) から  (N_8) を追加します。

  •  (N_1) 任意の  x \in N に対して  s(x) \ne x
  •  (N_2) 任意の  x \in N に対して  s(x) \ne x_0
  •  (N_3)  N 上で  s単射
  •  (N_4)  N 上で  \le は全順序
  •  (N_5)  N は無限集合
  •  (N_6)  X \subseteq N かつ  X \ne \varnothing ならば   X は極小元を持つ
  •  (N_7) 任意の  x \in N に対して  N_{\cong x} = \{x\}
  •  (N_8) 任意の  x \in N に対して  s(x) \not\le x

これらの条件により以下の表のようにタイプ  T_1 から  T_5 に分類することができます。

タイプ  N_1  N_2  N_3  N_4  N_5  N_6  N_7  N_8 図式
 T_1 = N_1 \land N_2 \land N_3  0 \to 1 \to \cdots
 T_2 = N_1 \land N_2 \land \neg N_3 × × × × × ×  0 \to 1 \to \cdots \to n \to \cdots \to n
 T_3 = N_1 \land \neg N_2 × × × × × ×  0 \to 1 \to \cdots \to 0
 T_4 = \neg N_1 \land N_2 × × × ×  0 \to 1 \to \cdots \to n \to n
 T_5 = \neg N_1 \land \neg N_2 × × × ×  0 \to 0

この表が成り立つことを以下で示します。

(P1)  x, y \in M x < y ならば  s(x) \le y

[証明] (O5)より  s^*(x) = \{x\} \cup s^*(s(x)) となりますが、 x \ne y なので  y \in s^*(s(x)) となり、 s(x) \le y となります。[証明終わり]

(P2)  x, y \in M x \le y ならば  s(x) \le s(y)

[証明]  x = y ならば  s(x) = s(y) \le s(y) x < y ならば(P1)より  s(x) \le y となり  s(x) \le y \le s(y) となります。[証明終わり]

(P3)  x, y \in M x < y かつ  s(x) = s(y) ならば  s^2(x) \le s(x)

[証明] (P1)より  s(x) \le y となり (P2)より  s^2(x) \le s(y) = s(x) となります。[証明終わり]

(P4)  x, y \in M x < y ならば  y = s(z) となる  z \ge x が存在する

[証明] (O5)より  s^*(x) = \{x\} \cup s^*(s(x)) となり、 y \ne x なので  y \in s^*(s(x)) となります。(O6)より  \bar{s}(s^*(x)) = s^*(s(x)) \ni y となるので  y = s(z) となる  z \ge x が存在します。[証明終わり]

(P5)  x, y \in N ならば  x \le y または  y \le x

[証明]  x = x_0 のときは  y \in N = s^*(x) より  x \le y となります。

 x \le y または  y \le x を仮定して  s(x) \le y または  y \le s(x) を示します。 x \le y のとき(O5)より  y \in s^*(x) = \{x\} \cup s^*(s(x)) y =x のとき(O8)より  y \le s(x) y \in s^*(s(x)) のとき(O7)より  s(x) \le y y \le x のとき(O8)より  y \le x \le s(x) となり  y \le s(x) が成り立ちます。

よって帰納法により主張が成り立ちます。[証明終わり]

表の内容の証明

(T1)  N_2 \land N_3 \implies N_4

[証明]  (N_2) 任意の  x \in N に対して  s(x) \ne x_0 (N_3)  N 上で  s単射を仮定して  (N_4)  N 上で  \le は全順序であることを示します。

まず半順序であることを示します。任意の  x, y \in N に対して  x \le y y \le x ならば  x = y であることを、帰納法でを示します。

まず  x = x_0 のときを示します。任意の  y \in N に対して  x_0 \le y y \le x_0 ならば  x_0 = y であることを帰納法で示します。

(P2)より  y < x_0 ならば  x_0 = s(z) となる  z \ge y が存在します。 (N_2) よりこのような  z は存在しないので  y = x_0 となります。

 x \in N に対して、任意の  y \in N に対して  x \le y y \le x ならば  x = y であるとき、任意の  y \in N に対して  s(x) \le y y \le s(x) ならば  s(x) = y であることを示します。

 s(x) \ne y と仮定すると、(P2)より  y = s(y') となる  y' \ge s(x) と、 s(x) = s(z) となる  z \ge y が存在します。 (N_3) より  x = z となります。 x \le s(x) \le y' \le s(y') = y \le z = x なので  x \le y' y' \le x となり仮定より  x = y' となります。よって  s(x) = s(y') = y となります。

帰納法により  \le が半順序であることが示されました。

(P5)より  \le は全順序となります。[証明終わり]

(T2)  N_1 \land N_4 \implies N_3

[証明]  (N_1) 任意の  x \in N に対して  s(x) \ne x (\neg N_3)  N 上で  s単射ではないと仮定して  (\neg N_4)  N 上で  \le は全順序ではないことを示します。

 (\neg N_3) より  x \ne y s(x) = s(y) となる  x, y \in N が存在します。(P5)より  x \le y または  y \le x となります。 x \le y とします。 x \ne y なので(P1)より  s(x) \le y となります。 s(y) = s(x) \le y y \le s(y) (N_1)より  s(y) \ne y となるので、 \le は半順序ではありません。[証明終わり]

(T3)  N_1 \land N_4 \implies N_2

[証明]  (N_1) 任意の  x \in N に対して  s(x) \ne x (\neg N_2)  x_1 \in N が存在して  s(x_1) = x_0 を仮定して  (\neg N_4)  N 上で  \le は全順序ではないことを示します。

 (\neg N_2) より  s(x_1) = x_0 となる  x_1 \in N が存在します。 (N_1) より  s(x_0) \ne x_0 となるので  x_1 \ne x_0 となって (P1)より  s(x_0) \le x_1 となります。よって  s(x_0) \le x_1 \le s(x_1) = x_0 となりますが、 x_0 \le s(x_0) s(x_0) \ne x_0 であるので  \le は半順序ではありません。[証明終わり]

(T4)  \neg N_1 \implies N_4

[証明]  (\neg N_1)  x_1 \in N が存在して  s(x_1) = x_1 を仮定して  (N_4)  N 上で  \le は全順序であることを示します。

 (\neg N_1) より  s(x_1) = x_1 となる  x_1 \in N が存在します。 x_1 = x_0 のときは  N = \{ x_0 \} となるので  \le は全順序となります。 x_1 \ne x_0 とします。

 x \in N に対して  N_{\le x} = \{ y \in N \mid y \le x \} とおきます。

 x, y \in N x < y とすると (P4)より  y = s(z) となる  z \ge x が存在します。

ここで  y \le x と仮定すると  y \le x \le z s(y) \le s(z) = y となり、 N_{\le y} \in \mathcal{R}_{x_0} となるので  N = N_{\le y} となります。よって  x_1 \le y y \in s^*(x_1) = \{x_1\} となります。また  x_1 \le y \le x となるので同様に  x \in s^*(x_1) = \{x_1\} となって、 x = x_1 = y となります。これは  x < y に矛盾となります。

よって  x \le y x \ne y ならば  y \le x とはなりません。

よって  x \le y かつ  y \le x ならば  x = y となり、 \le は半順序、(P5)より全順序となります。[証明終わり]

(T5)  N_2 \land N_3 \implies N_5

[証明]  (N_2) 任意の  x \in N に対して  s(x) \ne x_0 (N_3)  N 上で  s単射を仮定して  (N_5)  N は無限集合であることを示します。

 (N_3) より  s: N \to N単射で、 (N_2) より  \bar{s}(N) \subseteq N \setminus \{x_0\} となるので  s全射ではありません。よって  N は無限集合となります。[証明終わり]

(T6)  N_1 \land N_4 \implies N_6

[証明]  (N_1) 任意の  x \in N に対して  s(x) \ne x (N_4)  N 上で  \le は全順序を仮定して  (N_6)  X \subseteq N かつ  X \ne \varnothing ならば   X は極小元を持つことを示します。

 Y = \{ y \in N \mid 任意の \ x \in X \ に対して \ y \le x \} とおきます。任意の  x \in N に対して  x_0 \le x なので  x_0 \in Y となります。

 X \ne \varnothing より  x \in X が存在します。(O5)より  x \le s(x) (N_1) より  x \ne s(x) であり、 (N_4) より  \le は全順序なので  s(x) \not\le x となります。よって  s(x) \notin Y となり  Y \ne N となります。

よって

  •  0 \in Y かつ  Y \ne N

となり(O1)より

  • (*1)  y \in Y かつ (*2)  s(y) \notin Y

となる  y が存在します。(*2)よりある  x_1 \in X が存在して  s(y) \not\le x_1 となります。 (N_4) より  \le は全順序なので  x_1 < s(y)、よって  x_1 \le y となります。(*1)より任意の  x \in X に対して  y \le x なので  y \le x_1 となり、 (N_4) より  \le は全順序なので  y = x_1 \in X となります。よって (*1)より  y X の最小元となります。[証明終わり]

(T7)  N_4 \iff N_7

[証明] (P5)より
 (N_4)  N 上で  \le は全順序  \iff  \le は半順序
 \iff  (N_7) 任意の  x \in N に対して  N_{\cong x} = \{x\}
が成り立ちます。[証明終わり]

自然数の定義

 N とは別に、 \mathbf{N}^{(T_1)} N と同様に定義します。このとき  x_0 0 s \sigma として定義します。 \mathbf{N}^{(T_1)} (T_1) を満たすとします。
 \nu :  \mathbf{N}^{(T_1)} \to N
 \begin{cases}
\nu(0) = x_0 \\
\nu(\sigma(n)) = s(\nu(n)) & (n \ne 0)
\end{cases}
と定義します。 \nu(\mathbf{N}^{(T_1)}) \in \mathcal{R}_{x_0} となるので  \nu全射となります。

(N1)  N_{\le s(x)} = N_{\le x} \cup N_{\cong s(x)}

[証明]  N_{\le s(x)} \supseteq N_{\le x} N_{\le s(x)} \supseteq N_{\cong s(x)} が成り立つので  N_{\le s(x)} \supseteq N_{\le x} \cup N_{\cong s(x)} が成り立ちます。

 y \in N_{\le s(x)} \setminus N_{\le x} をとります。 y \le s(x) かつ  y \not\le x であるので、(P5)より  y \not\le x ならば  x < y となり(P1)より  s(x) \le y となります。よって  y \le s(x) かつ  s(x) \le y となり  y \in N_{\cong s(x)} となります。[証明終わり]

(N2)  n \in \mathbf{N}^{(T_1)} に対して  \mathbf{N}^{(T_1)}_{\le n} は有限集合

[証明]  \mathbf{N}^{(T_1)}_{\le 0} = \{ 0 \} となるので  \mathbf{N}^{(T_1)}_{\le 0} は有限集合となります。

 \mathbf{N}^{(T_1)}_{\le n} が有限集合と仮定します。(N1)、(T7)より  \mathbf{N}^{(T_1)}_{\le \sigma(x)} = \mathbf{N}^{(T_1)}_{\le n} \cup \mathbf{N}^{(T_1)}_{\cong \sigma(n)} = \mathbf{N}^{(T_1)}_{\le n} \cup \{\sigma(n)\} となり、(FM6)より  \mathbf{N}^{(T_1)}_{\le \sigma(n)} は有限集合となります。

よって帰納法により主張が成り立ちます。[証明終わり]

(N3) 集合  X が全順序  \le に関する最大元を持たないならば  X は無限集合

[証明]  X が最大元を持たないので任意の  x \in X に対して  x < y となる  y \in X が存在します。そのような  y の一つを  s(x) とおくことによって  s: X \to X を定義することができます。以前の議論と同様に、 s^*: X \to \mathfrak{P}(X) を定義します。 x_0 \in X をとります。 s s^*(x_0) への制限は単射となりますが、 x_0 は像に含まれないので全射ではありません。よって  s^*(x_0) は無限集合となり、 X も無限集合となります。[証明終わり]

(N4) 集合  X が全順序  \le に関する最小元を持たないならば  X は無限集合

[証明] (N3)と同様です。[証明終わり]

(T8)  N_5 \iff N_8

[証明]  (\Longrightarrow):  (\neg N_8)  x_1 \in N が存在して  s(x_1) \le x_1 であることを仮定して  (\neg N_5)  N は有限集合であることを示します。

 \nu全射なので(T6)より  x_1 = \nu(n) となる最小の  n \in \mathbf{N}^{(T_1)} が存在します。(N2)より  \mathbf{N}^{(T_1)}_{\le n} は有限集合なので(FM2)より  N = \nu(\mathbf{N}^{(T_1)}_{\le n}) は有限集合となります。

 (\Longleftarrow):  (N_8) 任意の  x \in N に対して  s(x) \not\le x であることを仮定して  (N_5)  N は無限集合であることを示します。

 (N_8) ならば  (N_1) 任意の  x \in N に対して  s(x) \ne x かつ  (N_2) 任意の  x \in N に対して  s(x) \ne x_0 となることは明らか。

 x < y かつ  y < x となる  x, y \in N が存在すると仮定すると、(P1)より  s(x) \le y となり、 s(x) \le y < x から  s(x) \le x となるので  (N_8) は成り立ちません。よって  (N_8) が成り立つならばそのような  x, y \in N は存在しないので  \le は半順序となり、(P5)より (N_4)  N 上で  \le は全順序となります。

よって(T2)より  (N_3)、(T5)より  (N_5) が成り立ちます。[証明終わり]

(T9)  N_5 \implies N_2

[証明]  (\neg N_2)  x_1 \in N が存在して  s(x_1) = x_0 を仮定して  (\neg N_5)  N は有限集合であることを示します。

 (\neg N_2) ならば  (\neg N_8) となるので、(T8)より  N は有限集合となります。[証明終わり]

(T10)  N_5 \implies N_3

[証明]  (\neg N_3)  N 上で  s単射ではないと仮定して  (\neg N_5)  N は有限集合であることを示します。

 (\neg N_3) より  x \ne y s(x) = s(y) となる  x, y \in N が存在します。(P5)より  x \le y または  y \le x となります。 x \le y とします。(P3)より  s^2(x) = s(x) となり(T8)より  N は有限集合となります。 y \le x の場合も同様です。[証明終わり]

(T11)  \neg N_2 \implies N_3

[証明]  (\neg N_2)  x_1 \in N が存在して  s(x_1) = x_0 を仮定して  (N_3)  N 上で  s単射であることを示します。

 (\neg N_2) ならば (T9)より  N は有限集合となります。(P4)より  y \ne x_0 ならば  y = s(z) となる  z \in N が存在します。よって  (\neg N_2) より任意の  y \in N に対して  y = s(z) となる  z \in N が存在するので  s全射となります。よって  s単射となります。[証明終わり]

(T12)  N_2 \land N_3 \implies N_1

[証明]  (\neg N_1)  x_1 \in N が存在して  s(x_1) = x_1 (N_2) 任意の  x \in N に対して  s(x) \ne x_0 を仮定して  (\neg N_3)  N 上で  s単射ではないことを示します。

 (\neg N_1) ならば  (\neg N_8) となるので、(T8)より  N は有限集合となります。 (N_2) より  s全射ではないので、単射ではありません。[証明終わり]

(T13)  N_4 \iff N_6

[証明]  (\Longrightarrow):  (N_4)  N 上で  \le は全順序であることを仮定して  (N_6)  X \subseteq N かつ  X \ne \varnothing ならば   X は極小元を持つことを示します。

 (N_4) が成り立つのは  (T_1) (T_4) (T_5) の場合となります。

 (T_1) の場合は(T6)より  (N_6) が成り立ちます。 (T_4) (T_5) の場合は(T9)、(T10)より  N は有限集合となります。(N4)より  (N_6) が成り立ちます。

 (\Longleftarrow):  (\neg N_4)  N 上で  \le は全順序ではないことを仮定して  (\neg N_6)  X \subseteq N かつ  X \ne \varnothing かつ極小元を持たない   X が存在することを示します。

 (N_4) が成り立たないは  (T_2) (T_3) の場合となります。このとき  (N_1) が成り立ちます。

 \le は全順序ではないとすると(P5)より半順序ではありません。よって  x < y かつ  y < x となる  x, y \in N が存在します。(P1)より  s(x) \le y となり、 s(x) \le y < x から  s(x) \le x となります。 (N_1) が成り立つので  s(x) \ne x となります。よって  \{x\} は極小元を持たないので  (N_6) は成り立ちません。[証明終わり]

以上で表の説明が終わりました。

  • (T1)  N_2 \land N_3 \implies N_4
  • (T2)  N_1 \land N_4 \implies N_3
  • (T3)  N_1 \land N_4 \implies N_2
  • (T4)  \neg N_1 \implies N_4
  • (T5)  N_2 \land N_3 \implies N_5
  • (T6)  N_1 \land N_4 \implies N_6
  • (T7)  N_4 \iff N_7
  • (T8)  N_5 \iff N_8
  • (T9)  N_5 \implies N_2
  • (T10)  N_5 \implies N_3
  • (T11)  \neg N_2 \implies N_3
  • (T12)  N_2 \land N_3 \implies N_1
  • (T13)  N_4 \iff N_6

集合と位相(増補新装版)(数学シリーズ)

集合と位相(増補新装版)(数学シリーズ)