「証明の“お膳立て”のやり方」、「証明の“お膳立て”のやり方 2： 証明の顧客・業者モデル」の続きです。このテの話は具体例がないとなかなかピンと来ないので事例を追加します。
内容：
証明要求の事例
A, Bを集合として、f:A→B は写像とします。この状況で次の命題を考えます。
- fは可逆 ⇔ fは全単射
この命題が真か偽か、現時点では分かりません。そこで、次の証明要求を発行します。
- Γ/ (A, B : Set), f:A→B |-? fは可逆 ⇔ fは全単射
証明要求とは、「証明できますか？」という疑問文、または「証明をしなさい」という（命令的）問題文です。証明可能性判断とは違って、証明の存在を保証してはいません。結局は証明できない（証明が存在しない）って事もあります。
Γ（大文字ガンマ）は、証明に使う諸々の予備知識・背景知識を表しています。`(A, B : Set)`は「A, Bを集合とする」を意味し、`f:A→B`は「fがAからBへの写像である」ことを述べています。記述が簡単になるように、`(A, B : Set), f:A→B`をΓに含めてしまって、以下、次のように書くことにします。
- Γ |-? fは可逆 ⇔ fは全単射
この証明要求（疑問文、問題文）に応える証明が在るにしろ無いにしろ、証明要求をより簡単な形に書き換えることは出来ます。これからその書き換えをします。証明要求は、証明という作業の仕様書・発注書のように考えることができます。このような比喩については「証明の“お膳立て”のやり方 2： 証明の顧客・業者モデル」に書いています。
証明要求の書き換えとは、論理の言葉で言えば、シーケント計算の一部を逆向きに実行することです。しかしここでは、形式的体系の話ではなくて、実際の非形式的証明（半形式的証明かな）のやり方として取り扱います。証明要求の書き換えは、本チャンの証明の事前準備と捉えています。よって、証明の“お膳立て”と呼んでいるのです。
“お膳立て”の全体像
証明要求「Γ |-? fは可逆 ⇔ fは全単射」に対する“お膳立て”をしてみると、作業ステップが意外と多いので、証明要求に番号を付けて整理します。枝番方式を採用します。番号付けルールは：
- 番号xの要求が2つの要求に分解されたときは、x-1, x-2 と番号を付ける。
- 番号xの要求が順次変形されていくときは、x → x.1 → x.2 → ... と番号を付けていく。
もとの証明要求にRと名前を付けて、お膳立ての作業進行に従って枝番を付けていくと、全体は次のようになります。
R
-----------------------------------------------[∧]
R-1 R-2
--------[⇒] -------[⇒]
R-1.1 R-2.1
--------[同値] -------[同値]
R-1.2 R-2.2
--------------------------[∧] -------[同値]
R-1.2-1 R-1.2-2 R-2.3
---------[同値] ----------[同値]
R-1.2-1.1 R-1.2-2.1
---------[∀] -----------[∀]
R-1.2-1.2 R-1.2-2.2
-----------[⇒]
R-1.2-2.3横線右に添えられているラベルは、証明要求の書き換え方法で、次の意味です。
- [∧] 結論が連言'∧'を含むとき、2つの証明要求に分解する。
- [⇒] 結論が含意'⇒'を含むとき、含意の前件（'⇒'の左側）を前提（'|-?'の左側）に移動する。
- [同値] 結論、または前提の命題を同値な命題で置き換える。
- [∀] 全称限量子を取り去り、前提に自由変数の型宣言を加える。
証明要求の書き換え
以下、上段に書き換え前（before）の証明要求、下段に書き換え後（after）の証明要求を書くフォーマットで書き換えを記述していきます。適宜、前節の全体像を参照してください。
RからR-1とR2への分解、R-1.2からR-1.2-1とR-1.2-2への分解は省略します。次の4つの部分を記述します。
- R-1 から R-1.2 まで
- R-2 から R-2.3 まで
- R-1.2-1 から R-1.2-1.2 まで
- R-1.2-2 から R-1.2-2.3 まで
R-1 から R-1.2 まで
(R-1) Γ |-? fは可逆 ⇒ fは全単射 --------------------------------------------[⇒] (R-1.1) Γ/ fは可逆 |-? fは全単射 --------------------------------------------[同値] (R-1.2) Γ/ fは可逆 |-? fは全射 ∧ fは単射
R-2 から R-2.3 まで
(R-2) Γ |-? fは全単射 ⇒ fは可逆 -------------------------------------[⇒] (R-2.1) Γ/ fは全単射 |-? fは可逆 ------------------------------------------[同値] (R-2.2) Γ/ fは全単射 |-? ∃g:B→A.(f;g = idA ∧ g;f = idB) ------------------------------------------[同値] (R-2.3) Γ/ fは全射, fは単射 |-? ∃g:B→A.(f;g = idA ∧ g;f = idB)
R-1.2-1 から R-1.2-1.2 まで
(R-1.2-1) Γ/ fは可逆 |-? fは全射 ------------------------------------------------------[同値] (R-1.2-1.1) Γ/ fは可逆 |-? ∀y∈B.∃x∈A.(f(x) = y) ------------------------------------------------------[∀] (R-1.2-1.2) Γ/ fは可逆, y : B |-? ∃x∈A.(f(x) = y)
R-1.2-2 から R-1.2-2.3 まで
(R-1.2-2) Γ/ fは可逆 |-? fは単射 --------------------------------------------------------------[同値] (R-1.2-2.1) Γ/ fは可逆 |-? ∀x, y∈A.(f(x) = f(y) ⇒ x = y) --------------------------------------------------------------[∀] (R-1.2-2.2) Γ/ fは可逆, (x, y : A) |-? f(x) = f(y) ⇒ x = y --------------------------------------------------------------[⇒] (R-1.2-2.3) Γ/ fは可逆, (x, y : A), f(x) = f(y) |-? x = y
証明に必要なこと
“お膳立て”の全体像は、上から下に広がるツリーの形をしています。最上部（ルート）がもとの証明要求です。末端（葉）が書き換えを終えた証明要求です。末端の証明要求だけを並べると次の3つです。
- (R-2.3) Γ/ fは全射, fは単射 |-? ∃g:B→A.(f;g = idA ∧ g;f = idB)
- (R-1.2-1.2) Γ/ fは可逆, y : B |-? ∃x∈A.(f(x) = y)
- (R-1.2-2.3) Γ/ fは可逆, (x, y : A), f(x) = f(y) |-? x = y
この3つの証明要求に応える証明を書けば、もとの証明要求に応えたことになります。(R-1.2-1.2)と(R-1.2-2.3)は簡単なので、証明のハイライトは(R-2.3)に対する証明です。
写像 f:A→B に対して、点ごとの逆像を対応させる写像 f*:B→Pow(A) を定義して、次の補題を利用するのがよいでしょう。（[追記]「証明の“お膳立て”のやり方」でもf*という記号を使いましたが、あっちは f*:Pow(B)→Pow(A)、今回は f*:B→Pow(A) なので違います。注意してください。[/追記]）補題の利用法については「証明の“お膳立て”のやり方 2： 証明の顧客・業者モデル」に書いてあります。
予備知識・背景知識の集合であるΓには、次の命題が入っているとします。
すべて論理記号を使って書くなら：
- ∀G:B→Pow(A).( (∀y∈B.(G(y) ≠ 空集合)) ⇒ ∃g:B→A.∀y∈B.(g(y)∈G(y)) )
この命題は選択公理と呼ばれる命題で、通常は証明なしに認めます。なので、Γに入れておきます。
ここまでお膳立てが済んでいるなら、残りの証明は難しくはないと思います。
