「証明の“お膳立て”のやり方 2： 証明の顧客・業者モデル」において、証明要求のターゲットに選言（論理OR）が入る場合に触れました。しかし、説明が不十分だったので補足します。また、前提に含まれる命題を推論規則として使う方法も説明します。
例題は、タイトルにある「随伴による集合差の定義」です。これは、それ自体としても面白い話題です。
内容：
- ターゲットに選言が含まれる証明要求のお膳立て
- 前提の命題を推論法則として使う
- 例題： 随伴による集合差の定義
- ターゲットが選言の場合のお膳立て
- 仮定を推論規則として使う
- バックワード・リーズニングによる証明
ターゲットに選言が含まれる証明要求のお膳立て
次の証明要求を考えます。（この書き方に対する詳細は、「証明の“お膳立て”のやり方 2： 証明の顧客・業者モデル」を参照。）
- Γ/ Δ |-? P∨Q
ここで、Γは論理式の集まり*1で、文脈（予備知識、背景知識）と呼びます。Δも論理式の集まりで仮定です。'|-?'の右側がターゲットで、2つの命題の選言の形です。この証明要求に応えるには、次の証明要求のどちらか一方に応えればいいのでした。
- Γ/ Δ |-? P
- Γ/ Δ |-? Q
しかし、選言の場合に証明要求を2つに分けるのはうまくいかないことが多いです。
「証明の“お膳立て”のやり方 2： 証明の顧客・業者モデル」の追記で、次の方法を紹介しました。
Γ/ Δ |-? P∨Q -------------------------[同値] Γ/ Δ |-? ¬(¬P∧¬Q) -------------------------[背理法] Γ/ Δ, ¬P, ¬Q |-? ⊥
この書き換えに続けて仮定に入った¬Qを、ターゲット側に戻すと：
- Γ/ Δ, ¬P |-? Q
お膳立ての手順としては、「選言の片方の否定を仮定に移す」となります。このお膳立ては実用性が高いものです。
前提の命題を推論法則として使う
（[追記]この節に対する補足説明が「証明の“お膳立て”のやり方 5： 証明可能性判断と推論規則」にあります。[/追記]）
証明要求の'|-?'の右側全体を前提と呼ぶと約束しました。前提は文脈と仮定を一緒にしたものです。その前提のなかに、次の形の命題が入っていることが多いですね。
- ∀x∈X.(P(x)⇒Q(x))
既知の定理とかはこの形で前提に含まれるでしょう。
上記の命題は、次のような証明可能性判断に書き換えてもいいです。
- (x : X), P(x) |- Q(x)
お膳立て手順としては、
Γ/ ∀x∈X.(P(x)⇒Q(x)), Δ |-? R --------------------------------------------[前提を判断に] Γ/ Δ |-? R Γ/ (x : X), P(x) |- Q(x)
別な言い方をすると、本チャンの証明のとき、(x : X), P(x) が出てきたら、Q(x) を推論して（導いて）いいということです。前提に入っている命題を、推論の規則として使うことになります。
この説明だけでは分かりにくいでしょうから、後で実例のなかで使ってみます。
例題： 随伴による集合差の定義
随伴は圏論の概念ですが、順序に関する随伴性はより単純です。「順序随伴性： ガロア接続の圏論」で述べています。順序随伴の例を挙げます（今引用した記事からの再掲）。
Xを集合、Pow(X)はXのベキ集合とします。W∈Pow(X) を選んで固定します。F, G:Pow(X)→Pow(X) を次のように定義しましょう。
- F(S) := S∩W
- G(S) := Wc∪S （(-)cは補集合）
このとき、次が成立します。
- F(S) ⊆ T ⇔ S ⊆ G(T)
このような関係にあるF, Gのペアを随伴ペア（adjoint pair）と呼びます。
もうひとつ別な例を挙げます。Wは同じく固定したPow(X)の要素です。
- F(S) := S＼W （集合の差）
- G(S) := S∪W
この場合、FとGは随伴ペアです。つまり、次が成立します。
- S＼W ⊆ T ⇔ S ⊆ T∪W
簡略に言うと、集合に関する差と和が随伴になっています。この「差と和の随伴性」をターゲット命題とします。証明要求は次のようになるでしょう。
- Γ/ (X : Set), (W : Pow(X)), (S, T : Pow(X)) |-? S＼W ⊆ T ⇔ S ⊆ T∪W
記述を簡略にするために、仮定（自由変数 X, W, S, T の型宣言）も文脈に詰め込んで、次の形にします。
- Γ |-? S＼W ⊆ T ⇔ S ⊆ T∪W
ターゲットが選言の場合のお膳立て
まずは、いつもどおりのお膳立てをしましょう。もう慣れてきたと思うので、証明要求の書き換え理由（根拠）は省略します。
Γ |-? S＼W ⊆ T ⇔ S ⊆ T∪W ---------------------------------------------------------------- Γ |-? S＼W ⊆ T ⇒ S ⊆ T∪W Γ |-? S ⊆ T∪W ⇒ S＼W ⊆ T ------------------------------- ------------------------------- Γ/ S＼W ⊆ T |-? S ⊆ T∪W Γ/ S ⊆ T∪W |-? S＼W ⊆ T
左下の証明要求について考えます。
- Γ/ S＼W ⊆ T |-? S ⊆ T∪W
ターゲットは ∀x∈X.(x∈S ⇒ x∈T∨x∈W) と書けるので：
Γ/ S＼W ⊆ T |-? S ⊆ T∪W ----------------------------------------------- Γ/ S＼W ⊆ T |-? ∀x∈X.(x∈S ⇒ x∈T∨x∈W) ----------------------------------------------- Γ/ S＼W ⊆ T, (x : X) |-? x∈S ⇒ x∈T∨x∈W ----------------------------------------------- Γ/ S＼W ⊆ T, (x : X), x∈S |-? x∈T∨x∈W
ここで、ターゲットが選言である形が登場しました。「選言の片方の否定を仮定に移す」変形を施すと：
- Γ/ S＼W ⊆ T, (x : X), x∈S, ¬(x∈W) |-? x∈T
ここまで来てしまうと、直感でも分かる気はしますが、論理的な推論（リーズニング）を続けます。
仮定を推論規則として使う
前節最後の証明要求には、S＼W ⊆ T という仮定がありました。これは次の命題と同じです。
- ∀x∈X.(x∈S∧¬(x∈W) ⇒ x∈T)
この命題を証明可能性判断の形で、証明要求と並べて書くと：
- （判断） Γ/ (x : X), x∈S, ¬(x∈W) |- x∈T
- （要求） Γ/ (x : X), x∈S, ¬(x∈W) |-? x∈T
んっ、アレ、証明のお膳立てをしてるうちに証明が終わってしまったよ。要求されていた証明が、最初の仮定のなかに（命題の形で）そっくり入っていたわけです。
残っている証明要求も見てみましょう。
Γ/ S ⊆ T∪W |-? S＼W ⊆ T --------------------------------------------------- Γ/ S ⊆ T∪W |-? ∀x∈X.(x∈S∧¬(x∈W) ⇒ x∈T) --------------------------------------------------- Γ/ S ⊆ T∪W, (x : X) |-? x∈S∧¬(x∈W) ⇒ x∈T --------------------------------------------------- Γ/ S ⊆ T∪W, (x : X), x∈S, ¬(x∈W) |-? x∈T
仮定のなかに S ⊆ T∪W がありますが、これは次の証明可能性判断として書けます。
- (x : X), x∈S |- x∈T∨x∈W
証明可能性判断においても「選言の片方の否定を仮定に移す」は使えます。
- (x : X), x∈S, ¬(x∈W) |- x∈T
仮定の命題を証明可能性判断に書き換えた全体は：
- Γ/ (x : X), x∈S, ¬(x∈W) |- x∈T
これまた証明が終わってしまいました（もう、やることがない）。
バックワード・リーズニングによる証明
今回の例では、証明のお膳立てをしているうちに、やることがなくなってしまいました。つまり、本チャンの証明部分がないのです。
こうしてみると、証明のお膳立てと本チャンの証明という区別はさして意味がないことが分かります。実は、今まで“証明のお膳立て”と呼んでいた行為は、ターゲット（結論）をより簡単な形に分解していくスタイルの“証明”でもあるのです。このスタイルの証明（行為）をバックワード・リーズニングと呼びます。ターゲットを作り出すスタイルのほうがフォワード・リーズニングです。
人間は、フォワード・リーズニングとバックワード・リーズニングを組み合わせて証明行為を実行しています。証明支援系（ソフトウェア）では、バックワード・リーズニングだけをサポートしているものが多数派です。人間による証明でも、バックワード・リーズニング、すなわちお膳立て方式で全てを済ましてしまうことも可能です（今回の例）。とはいえ、フォワード・リーズニングを禁止されると辛いので、バックワード／フォワードを柔軟に組み合わるのが得策です。
*1:論理式のあいだには依存関係があるので、単なる集合ではありません。依存関係を順序とした順序集合とみなすとよいでしょう。
