N君が「こういうのは、どうやって証明したらいいのか… わかんないなー？」と困った顔をしてました。的確な処方箋を述べることは出来ないのですが、ヒントになりそうなことを記しておきます。
目的：
シリーズ目次：
- 証明の“お膳立て”のやり方
- 証明の“お膳立て”のやり方 2： 証明の顧客・業者モデル
- 証明の“お膳立て”のやり方 3： さらに事例
- 証明の“お膳立て”のやり方 4： 随伴による集合差の定義
- 証明の“お膳立て”のやり方 5： 証明可能性判断と推論規則
- 証明の“お膳立て”のやり方 オマケ1： 集合の内包的記法の困惑
- 有限集合とは何だろう（ストーリー付き練習問題集）
- 有限集合とは何だろう への補足
- 距離空間と位相空間と連続写像 // 2つの連続性が同値であること （お膳立ての例）
全称と存在を使った証明のやり方
証明の“お膳立て”とは
何らかの命題を証明するとき、状況を確認したり、仮定と結論を整理したり、命題をより扱いやすい形に変形したりします。こういうことも証明行為（リーズニング）の一部だといえますが、プリプロセス（前段階の処理）っぽい雰囲気があるので、ここでは“お膳立て”と呼んでおきましょう。
簡単な証明なら出来るけど、少し複雑になると「どこから手を付けていいか分からない」という人は、このお膳立てがうまくいってないことがあるように思えます。
とはいえ、お膳立てを正確に定義することも、体系的に手順・コツを提示することも出来ないので、具体的な例に沿って、その例のなかに出てくる幾つかの手法を説明します。
例題
f:A→B は写像とします。Pow(B)は、集合Bのベキ集合（powerset）です。つまり、S∈Pow(B) ⇔ S⊆B ですね。f*:Pow(B)→Pow(A) は、Bの部分集合に“fによる逆像”を対応させる写像です。詳しく言えば：
- f*(S) = {x∈A | f(x)∈S}
f*はf-1と書かれることが多いですが、fの逆写像ではないので上付きアスタリスクにします。
さて、次の命題を例に使います。
この命題を普通の方法（集合と写像に関する議論）で証明することを考えます。
命題、証明可能性判断、証明要求
ある命題（形式的に扱う場合は論理式）Qに対して、それが証明可能であることを意味するメタ命題を次の形に書きます。
- |- Q
この形のメタな主張を証明可能性判断（provability judgement）と呼びます。「Pが証明できる」ということを記号的に書いただけです。
P1, ..., Pn という幾つかの命題を仮定としてQを証明できることは、次のように書きます。
- P1, ..., Pn |- Q
一般的には、Qを証明するために必要な仮定命題はイッパイあります。それを全部並べると大変なので、暗黙の予備知識のような命題までは書き並べません。ここでは、特に注目してない諸々の前提達をΓ（大文字ガンマ）で表します。Γは命題の集合だと思ってください。例えば、全射・単射の定義とか、x∈A ⇒ f(x)∈B のような当たり前な命題は全てΓに入っているとします。ここだけの用語法ですが、特に注目している仮定命題を単に「仮定」と呼び、暗黙の予備知識なども含めた全体を「前提」と呼びます。
扱っている命題が地の文と紛らわしいときは、命題をバッククォートで囲むことにします。例えば、`x∈A ⇒ f(x)∈B`のように。
命題Pが証明可能かどうかは分かってない状態で、「証明できるでしょうか？」という疑問文、あるいは「証明を試みてください」という問題文の記述として、次の形を使うことにします。
- |-? Q
使ってよい仮定、あるいは暗黙の前提も指定した形は：
- P1, ..., Pn |-? Q
- Γ, P1, ..., Pn |-? Q
この形を証明要求（proof requirement）と呼ぶことにします。
前節で述べた例題を証明要求として書けば：
Γは使ってもよい諸々の前提だとします。`Aは集合`とか`∀S∈Pow(B).∀x∈A.(x∈f*(S) ⇔ f(x)∈S)`などもΓに入っているでしょう。暗黙の前提Γはけっこう膨大になったりします。
連言の分解
最初のお膳立ては、証明すべき命題（ゴール、ターゲット）が連言（論理AND）で書かれているとき、証明要求を2つ（以上）に分解することです。
`f:A→B は全射 ⇔ f*:Pow(B)→Pow(A) は単射`という命題には、連言が入っています。なぜなら、`P ⇔ Q`は、`(P⇒Q)∧(Q⇒P)`のことだからです。連言（'∧'）を明示的に書けば：
もとの証明要求は、次の2つの証明要求になります。
一般的には、P∧Qがターゲットである証明要求は、Γ |-? P と Γ |-? Q に分解（decompose, resolve）できます。上段に分解前（before）、下段に分解後（after）を書く書式で表現すれば：
Γ |-? P∧Q ----------------------[連言の分解] Γ |-? P Γ |-? Q
含意の変形
しばらくは、2つに分解した片一方の証明要求に注目しましょう。
証明すべき命題に含意記号（'⇒'）が含まれます。このとき、含意の前件（antecedent, 左側）を、証明要求の仮定側に移してかまいません。つまり、証明要求を次の形に変形*1していいのです。
一般的なお膳立てルールとしては：
Γ |-? P⇒Q --------------[含意の変形] Γ, P |-? Q
これは、演繹定理（deduction theorem）と呼ばれる、論理の基本法則です。定理と呼んでいますが、これが成立するように証明系を設計するので、論理の指導原理（のひとつ）と言ってもいいでしょう。実際、証明のお膳立てには演繹定理が頻繁に使われます。
なお、演繹定理の圏論的解釈は、順序随伴性： ガロア接続の圏論に書いています。
全称限量子を型宣言に
証明すべき命題`f*:Pow(B)→Pow(A) は単射`が持つ情報のうちで、証明要求の前提側（'|-?'の左側）に持っていけるものを移動すると：
- Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)` |-? `∀S, T∈Pow(B).(f*(S) = f*(T) ⇒ S = T)`
全称限量子'∀'が出てきました。全称限量子の束縛変数S, Tは、ベキ集合Pow(B)上を走る自由変数に置き換えることができます。自由変数の変域を変数の型と考えて、次の形式を使うことにします。
- S, T : Pow(B)
意味はもちろん、「SとTは自由変数で、その型（変域）はPow(B)である」です。これは、`S : Pow(B)`, `T : Pow(B)` の略記である点にも注意してください。
全称限量子を取り払い、束縛変数を自由変数に置き換え、その変数の型宣言を前提側に置く、という証明要求の変形が許されます。
- Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)` |-? `f*(S) = f*(T) ⇒ S = T`
一般的なお膳立てルールとしては：
Γ |-? ∀x∈X.Q ------------------[全称の変形] Γ, x : X |-? Q
お膳立てルールの繰り返し適用
現時点での証明要求のターゲットに含意'⇒'が出現するので、もう一度、含意の変形ルールを適用します。すると：
- Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)` |-? `S = T`
これでターゲットは`S = T`になりました。SとTは集合なので、S = T ⇔ S⊆T ∧ T⊆S です。`S = T`を同値な命題で置き換えると：
- Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)` |-? `S⊆T ∧ T⊆S`
連言の分解ルールを適用すると：
- Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)` |-? `S⊆T`
- Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)` |-? `T⊆S`
ターゲットに含まれる包含（'⊆'）を定義により展開すれば：
- Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)` |-? `∀y.(y∈S ⇒ y∈T)`
- Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)` |-? `∀y.(y∈T ⇒ y∈S)`
さらに全称の変形と含意の変形を適用すると：
- Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)`, `y : Any`, `y∈S` |-? `y∈T`
- Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)`, `y : Any`, `y∈T` |-? `y∈S`
`y : Any`は、yが制約のない自由変数であることを表します。しかし、直後に`y∈S`があるので、まとめて`y : S`としても同じことです。
ここまで証明要求を変形すれば、使える仮定はだいぶ増えているし、証明すべき結論は簡単な形をしているので、証明が出来そうな気がします。
今までのお膳立ての手順を見てみると、これはバックワード・リーズニングによる証明行為を遂行していることになります。あえて“お膳立て”として証明本体と区別しているのは、証明は通常、フォワード・リーズニングとして書かれるからです。バックワード・リーズニングは、事前調査や予備作業の位置付けになることが多いでしょう。
ちなみに、人間はバックワード・リーズニングを補助的に使い、オフィシャルな証明記述にはフォワード・リーズニングを使いますが、コンピュータによる証明ではバックワード・リーズニングだけを使うほうが主流です。
同値な命題に置き換える
ここで話を戻して、保留にしておいた証明要求を再び取り上げます。
この命題は対偶にしたほうがやりやすい気がするので、結論を対偶に置き換えます。対偶に置き換えなきゃダメなわけじゃありませんが、わずかに証明が簡略化するし、置き換えの事例としてやってみます。あと、`f*:Pow(B)→Pow(A)`は前提側に移します。
一般的なお膳立てルールとしては：
Γ |-? P ⇒ Q --------------------[対偶に置き換え] Γ |-? ¬Q ⇒ ¬P
対偶に限らず、証明要求の結論や前提に出てくる命題を同値な命題に置き換えることは許されます。既に、定義による置き換えなどは使っていますし。
お膳立てを完成させる
この証明要求の結論にも'⇒'が登場するので、前件を前提側に移します。
単射の定義を使って結論を同値な命題に置き換えれば：
- Γ, `f*:Pow(B)→Pow(A)`, `f:A→B は全射ではない` |-? `¬(∀S, T∈Pow(B).(f*(S) = f*(T) ⇒ S = T))`
さらに、ドモルガンの法則を使って結論を同値な命題に置き換えます。
- Γ, `f*:Pow(B)→Pow(A)`, `f:A→B は全射ではない` |-? `∃S, T∈Pow(B).(f*(S) = f*(T) ∧ S ≠ T)`
あっ、P⇒Q と ¬P∨Q が同値なことも使っています。
さて、今までの経緯をまとめましょう。最初の証明要求は次でした。
証明要求に対して許される幾つかの操作を適用することにより、次の3つの証明要求にたどり着きました。
- Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)`, `y : Any`, `y∈S` |-? `y∈T`
- Γ, `f:A→B は全射`, `f*:Pow(B)→Pow(A)`, `S, T : Pow(B)`, `f*(S) = f*(T)`, `y : Any`, `y∈T` |-? `y∈S`
- Γ, `f*:Pow(B)→Pow(A)`, `f:A→B は全射ではない` |-? `∃S, T∈Pow(B).(f*(S) = f*(T) ∧ S ≠ T)`
1番目と2番目はほとんど同じ形をしているので、どっちか一方を証明して「同様に」でいいと思います。3番目は、結論（ターゲット）が存在命題なので、当該条件を満たすS, Tを実際に構成する問題になります。
これら3つの証明要求は、もとの証明要求に比べれば、だいぶ取り扱いやすくなっています。やりやすい状況まで質問や問題設定（つまり証明要求）を書き換えることが、今回“お膳立て”と呼んだ作業です。お膳立ては済んだので、3つの証明要求に応える、つまり実際の証明を行ってみてください。
*1:分解と変形を区別して使っていますが、「分解」を"resolve"の訳語とするなら、すべて分解と呼んでしまってもいいかも知れません。
