有限集合とは何だろう への補足

「有限集合とは何だろう（ストーリー付き練習問題集）」にちょっと補足します。Xが有限のとき、S⊆X である集合Sは有限集合ですが、このことを示すストーリーに触れます。

内容：

余談：宇都宮市民の髪の毛の本数

Wikipeiaの「鳩の巣原理」の項目に、「ロンドンには、同じ本数の髪の毛を持った少なくとも2人の人間が存在する」の証明が載っています。

この証明の根拠になっているのは次の（現実世界の）事実です。

• 人の髪の毛の本数は15万本ほどである。
• ロンドンの人口は100万人以上である。
• 100万本以上の髪の毛を持つ人はいない。

これらの事実に鳩の巣原理を適用して結論を得ます。

人口100万はかなり安全にみた数で、人口50万でも大丈夫でしょう。つまり、50万本以上の髪の毛を持つ人はいないとします。餃子しか思い浮かばない宇都宮市*1でも50万以上の人口があるので、次の命題は成立します。

• 宇都宮市には、同じ本数の髪の毛を持った少なくとも2人の人間が存在する

[m]の部分集合に関する補題

「有限集合とは何だろう（ストーリー付き練習問題集）」で話題にした中心的な命題は次でした。

• 集合Xは有限 :⇔ ∃n∈N.( X [n] ) ---(有限集合の定義)
• ∀X:Set.∀n, m∈N.( (X [n] ∧ X m) ⊃ n = m ) ---(基数の一意性)

この2つをまとめて書くために、一意存在を意味する'∃!'を使うと便利です。∃!x.P(x) の意味は、∃x.P(x) ∧ ( P(x)∧P(y) ⊃ x = y ) です。単なる存在命題より強い命題（きつい条件）になります。

• ∀X:Set.( Xは有限集合 ⊃ ∃!n∈N.( X [n] ) ) ---(有限集合に対する基数の一意存在)

これから、「集合として同型」と「基数が同じ」が同値であることが分かります。つまり、次が成立します。

• ∀X, Y:Set.( X, Yは有限 ⊃ ( X Y ⇔ ∃n∈N.( X [n] ∧ Y [n]) ) )

含意を記号'⊃'で表しているのに、同値は'⇔'でバランス悪いんだけど勘弁してね（バランスをとるなら、'⊂⊃'かな？）。

さて、集合として同型でない状況を分析するときは、次の命題がキーになります。

• ∀S:Set.∀m∈N.( S⊆[m] ⊃ ∃n∈N.( S [n] ∧ n ≦ m ) )

自然言語で書くならば：

• Sは集合だとして、自然数mに対して S⊆[m] ならば、S [n] かつ n ≦ m であるような自然数nが存在する。

これが正しいなら、[m]の部分集合は有限集合であり、その基数はm以下であることがわかります。

これから、基数の大小に関する次の命題も導けます。

• X, Yが有限集合のとき、X⊆Y ならば、Xの基数はYの基数以下である。

もっと一般化すれば：

• X, Yが有限集合のとき、XからYへの単射が存在するならば、Xの基数はYの基数以下である。

証明要求とその書き換え

前節で提示した命題 ∀S:Set.∀m∈N.( S⊆[m] ⊃ ∃n∈N.( S [n] ∧ n ≦ m ) ) を証明しましょう。数学的帰納法を使うと、当たり前すぎる命題でも証明できることが多いので、数学的帰納法でやっつける方針で。

まず、今問題にしている命題をターゲット命題とする証明要求を次の形に書ます。

 Γ/ S:Set |-? ∀m∈N.(
                  S⊆[m]
                  ⊃
                  ∃n∈N.(
                      S  [n] ∧ n ≦ m
                  )
                )

変数mに注目して、ターゲット命題を ∀m∈N.P(m) の形だと読みます。すると、数学的帰納法のベースとステップは次のようになります。

• ベース： S⊆[0] ⊃ ∃n∈N.( S [n] ∧ n ≦ 0)
• ステップの前件： S⊆[k] ⊃ ∃n∈N.( S [n] ∧ n ≦ k )
• ステップの後件： S⊆[k + 1] ⊃ ∃n∈N.( S [n] ∧ n ≦ k + 1 )

ベースのほうは、n = 0 として示せます。すると、課題（＝証明要求）はステップだけになります。ステップの前件を前提（'|-?'の左側）に、ステップの後件をターゲットにすれば、次の証明要求となります。

 Γ/ S:Set, k:N,
     S⊆[k] ⊃ ∃n∈N.( S  [n] ∧ n ≦ k )
  |-?
     S⊆[k + 1] ⊃ ∃n∈N.( S  [n] ∧ n ≦ k + 1 )

“ステップの後件の前件”も証明要求の前提側に移動すれば：

 Γ/ S:Set, k:N,
     S⊆[k] ⊃ ∃n∈N.( S  [n] ∧ n ≦ k ),
     S⊆[k + 1]
  |-?
     ∃n∈N.( S  [n] ∧ n ≦ k + 1 )

ターゲットは存在命題なので、条件にみあう自然数nを構成または検索すればいいことになります。

集合のあいだの同型の構成

前節で、∀S:Set.∀m∈N.( S⊆[m] ⊃ ∃n∈N.( S [n] ∧ n ≦ m ) ) に対する証明要求を書き換えて、ターゲットは次の命題としました。

• ∃n∈N.( S [n] ∧ n ≦ k + 1 )

S [n] を定義に従って展開すれば：

• ∃f:S→[n], g:[n]→S.(f;g = id_S ∧ g;f = id_[n] )

したがって、整数nと共に、上記を満たす写像f, gも構成しなくてはなりません。

証明要求の前提に S⊆[k + 1] が入っています。つまり、S ⊆ {0, 1, ..., k} です。k∈S か ¬(k∈S) のどちらかは常に成立します（排中律）。¬(k∈S) ならば、S⊆[k] となります。つまり、次は必ず成立します。

• S⊆[k] ∨ k∈S

S⊆[k] のときは、前提に入っている帰納法のステップの前件から S [n] ∧ n ≦ k であるnの存在がいえます。残りは、k∈S のときにターゲットを示すことだけです。

S' = S＼{k} （'＼'は集合の差）と置くと、S'⊆[k] となるので、再び帰納法のステップの前件から S' [n'] ∧ n' ≦ k となるn'があります。となると、ターゲットはさらに絞れて、次の証明要求として書けます。

• Γ'/ ¬(k∈S'), S' [n'], S = S'∪{k} |-? S [n' + 1]

ここで、Γ'は適当に調整した文脈（背景知識となる前提）です。前提にある S' [n'] から次のような f', g' の存在は保証されています。

• f':S'→[n'], g':[n']→S', f';g' = id_S', g';f' = id_[n']

これらをもとに、次のような f, g を作れば要求は満たせます。S = S'∪{k}, n = n' + 1 である点に注意してください。

• f:S'∪{k}→[n' + 1], g:[n' + 1]→S'∪{k}, f;g = id_S, g;f = id_[n]

f, gは次のように構成（定義）します。

• f(i) := if (i < k) then f'(i) else n'
• g(j) := if (j < n') then g'(j) else k

elseの部分を分かりやすく書くと、f(k) = n', g(n') = k です。こうして作った（構成した）f, gが、f;g = id_S, g;f = id_[n] を満たすのはすぐに分かるでしょう。

おわりに

やってみたことは、我々が直感的に当たり前だと思っていることを、適当な演繹系〈証明系 | 論理系〉のなかで証明できることを示す（実際の証明を構成する）ことです。得られる結果は「当たり前」なので、あんまり面白くないです。

「結果が面白くない」以外に、このテの話の問題点は、前提とターゲットの区別が付きにくいことです。まだ証明されてないターゲットも、内容的には当たり前なので、前提だと勘違いしがちです。

証明支援系を使うと勘違いは防げますが、お気軽に使える証明支援系がないのがまた困った話です。うーむ。

*1:宇都宮市を選んだのは僕が栃木県出身だから。