証明の“お膳立て”のやり方 2： 証明の顧客・業者モデル

昨日の記事「証明の“お膳立て”のやり方」の続きを書きます。発展編と言えるかも知れません。

昨日“お膳立て”という言葉を使った理由は、形式的論理体系の話ではなく、コンピュータによる証明の話でもなく、人間が例えば「f:A→B は全射 ⇔ f^*:Pow(B)→Pow(A) は単射」のような命題を手動で証明するときの“やり方”に関わる話だったからです。

今回も“やり方”の話です。メイヤー流の顧客・業者モデルを導入して、“お膳立て”の意義を確認・整理したいと思います。

内容：

• 第1回とシリーズ目次

文脈知識と仮定

証明可能性判断（provability judgement）から話を始めます。証明可能性判断は次の形に書くのでした。

• P₁, ..., P_n |- Q

nは任意の自然数なので、もの凄く大量の仮定があってもかまいません。しかし、通常は2,3個の仮定を書く程度でしょう。実際にはその他の仮定があっても、それは暗黙の仮定として書かないと思います。

この暗黙の仮定のために、事情が不透明になることがあるので、証明可能性判断の左側にはすべての仮定を書くことにします。しかし、明示的な仮定と暗黙の仮定を分けて次のように書きます。

• R₁, ..., R_k/ P₁, ..., P_n |- Q

R₁, ..., R_k が暗黙の仮定（って、もはや暗黙じゃないけど）で、P₁, ..., P_n が明示的仮定です。R₁, ..., R_k をΓのようなギリシャ文字大文字で表すことにします。

• Γ/ P₁, ..., P_n |- Q

Γのことを予備知識、背景知識、文脈知識などと呼びます。単に背景（background）、文脈（context; コンテキスト）とも言います。スラッシュより右に書く明示的仮定は単に仮定と呼びましょう。そして、'|-'の左側全体を前提（premises）と呼ぶことにします。証明要求においても同じ用語法を使います。

文脈知識と仮定の区別は、便宜的・恣意的なもので、確たる根拠はありません。したがって、スラッシュの位置はどこに移動してもかまいません。区切り（スラッシュ）の位置を変えてもいいことは次のように表現できます。

   Γ, R/ P1, ..., Pn |- Q
 ----------------------------[文脈から仮定へ]
   Γ/ R, P1, ..., Pn |- Q


   Γ/ P1, P2, ..., Pn |- Q
 ----------------------------[仮定から文脈へ]
   Γ, P1/ P2, ..., Pn |- Q

この事情は証明要求（proof requirement）のときも同じです。

   Γ, R/ P1, ..., Pn |-? Q
 ----------------------------[文脈から仮定へ]
   Γ/ R, P1, ..., Pn |-? Q


   Γ/ P1, P2, ..., Pn |-? Q
 ----------------------------[仮定から文脈へ]
   Γ, P1/ P2, ..., Pn |-? Q

文脈知識と仮定の境界線を動かしてもいいことは、理論的にはたいした意味はないです。そもそもそんな区別はしないのが普通です。しかし、現実的にはけっこう意味があって、境界線とその移動に対して意識的・自覚的になったほうがいいと思います。文脈知識（＝暗黙の仮定）がズレていてコミュニケーションがうまくいかない事態は頻繁に起きます。区切り（スラッシュ）位置の調整と合意がコミュニケーションでは重要なのです。

ターゲットからの論理記号の除去

証明要求において、'|-?'の右に書く命題（論理式）をターゲット（target）と呼ぶことにします。ゴールでも同義ですが、証明支援系における「ゴール」が甚だしく混乱しているので、「ゴール」という言葉は避けます。

さて、与えられた証明要求に対してお膳立て（事前処理）を施す主な動機は、証明要求のターゲットをより簡単にしたいことです。ターゲットに論理記号がたくさん含まれれば複雑な論理式ですから、論理記号を減らそうと試みるのです。

論理記号（慣用のもの）には、次があります。

1. ∧
2. ∨
3. ¬
4. ⇒
5. ∀
6. ∃

このなかで、∧, ⇒, ∀を除去するお膳立てルール（＝バックワード・リーズニングのルール）は「証明の“お膳立て”のやり方」で述べました。念のために再掲します。Γは文脈、Δは（明示的）仮定です。

      Γ/ Δ |-? P∧Q
 ------------------------------[連言の分解]
  Γ/ Δ |-? P   Γ/ Δ |-? Q

  Γ/ Δ |-? P⇒Q
 ------------------[含意の変形]
  Γ/ Δ, P |-? Q

  Γ/ Δ |-? ∀x∈X.Q
 ----------------------[全称の変形]
  Γ/ Δ, x : X |-? Q

ターゲットに ∨, ¬, ∃ が含まれる場合はどうでしょうか？ 次節以降で考えてみます。

背理法を使うとき

背理法を使うときは、事前に「背理法で証明します」のように断りを入れます。この断り書きは、お膳立ての一種です。お膳立てとは証明要求の変形ですが、背理法を使う直前に次の変形が行われるのです。

  Γ/ Δ |-? ¬Q
 -------------------[背理法]
  Γ/ Δ, Q |-? ⊥

ここで、'⊥'は矛盾を表す記号です。具体例として、「√2は有理数ではない」の証明要求で考えてみると：

  Γ/ |-? `¬(√2は有理数)`
 -----------------------------[背理法]
  Γ/ `√2は有理数` |-? 矛盾

もともとの証明要求は、諸々の予備知識Γから、`¬(√2は有理数)`を証明せよ、と要求しています。これを、予備知識Γと仮定`√2は有理数`から矛盾を証明せよ（矛盾を導き出せ）、と変形しています。

「お膳立てで論理記号を減らす」という動機から見ると、もともとはターゲットに否定'¬'が含まれていたのが、変形後に'¬'が消えているので、背理法のお膳立ては、否定記号を除去するお膳立てだと言えます。

証明における顧客と業者

メイヤー先生は、ソフトウェア仕様に関して、顧客（customer）と業者（provider, supplier）のあいだの契約（contract）という比喩を導入しました。この比喩的モデルは実に秀逸で、ソフトウェア仕様の基本概念を日常的な感覚で理解できるようになりました。興味がある方は、例えば次の記事を見てください。

• メイヤー流の契約となんでもケーキ屋さん
• メイヤー流の契約のあいだの強弱関係

証明においても、顧客・業者モデルを導入してみましょう。証明を請け負う“証明屋”という業者がいるとします。顧客は、業者“証明屋”に証明の作成を依頼します。業者は、顧客の依頼に応えて、成果物を納品します。依頼するときに契約が交わされ、納品時に契約が履行されたことが確認されます。

証明依頼のときの指示書・仕様書が、今話題にしている証明要求です。成果物＝納品物が証明です。ここでいう証明は、形式的な証明オブジェクト／タクティク言語で書かれた証明スクリプト／自然言語で書かれた伝統的証明などで、顧客と業者のあいだで合意があるならフォーマットは自由に選べます。

顧客と業者のあいだの契約の条件は、全て証明要求に書き込まれています。したがって、納品物のチェックも証明要求を基準にします。証明要求が Γ/ Δ |-? Q だとして、次の事は契約違反になります。

• ΓにもΔにも入ってない命題が仮定として使われた。
• Qと異なる命題が結論になっている。

より大枠に関する契約違反としては：

• 納品された証明のフォーマットが合意されたものではない。
• 納品された証明のなかに、顧客が解釈できない部分／許容できない部分がある。

上記のような不備がなければ、納品チェックはパスして、契約は履行されたとみなされます。

今話題にしている“お膳立て＝証明要求の書き換え”は、（世間によくある）元請け・下請けを考えれば理解できます。元請けが下請けに発注（再依頼）するとき、指示書・仕様書は書き換えられます。“丸投げ”ってヤツもありますが、ここでは丸投げは考えません。

例えば、次の“お膳立て＝証明要求の書き換え”を考えてみます。

      Γ/ Δ |-? P∧Q
 ------------------------------[連言の分解]
  Γ/ Δ |-? P   Γ/ Δ |-? Q

もとの証明要求を2つに分解し、2つの下請け業者に発注します。上がってきた下請け成果物をまとめれば、もとの証明要求を満たす成果物を顧客に納品できる、というわけです。

インテグレーターの憂鬱

ソフトウェア業界には、システムインテグレーターと呼ばれる業種があります。顧客と契約を交わす元請けと思えばいいでしょう。証明業界（架空の業界）にもインテグレーターがいるとしましょう。証明インテグレーターは、顧客からの証明要求を若干書き換えて下請け業者に発注します。下請けへの発注では、もとの証明要求よりは簡単な要求にします -- 良心的ですね*1。

ターゲットに、∧（連言）, ⇒（含意）, ∀（全称）, ¬（否定）を含む証明要求を、より簡単（論理記号が減っている）証明要求にして下請けに出すのは割とスンナリいきます。しかし、∨（選言）と∃（存在）の“お膳立て＝証明要求の書き換え”はちょっと難しい。

Γ/ Δ |-? P∨Q の形の、ターゲットが選言'∨'を含む証明要求の場合も、2つの証明要求に分解はできます。

1. Γ/ Δ |-? P
2. Γ/ Δ |-? Q

しかし、連言の場合とは違います。下請けに出した後の納品待ちがまったく違うのです。連言'∧'の場合は、2つの下請け業者両方の納品を待ちますが、選言'∨'の場合は、どちらか一方から納品があれば（もう一方を待たずに）、ただちに顧客への納品を完了させます。

余談ですが、'∧'と'∨'に関する下請けへの出し方／待ち方は、並列プロセスの制御方法と類似しています。証明行為とプログラム実行に何らかの関係があることを示唆しています。

さて、残るはターゲットが'∃'を含む証明要求です。どのように“お膳立て＝証明要求の書き換え”をして下請けに出せばいいのでしょうか？

存在'∃'が付く命題は、選言'∨'がイッパイある命題と思えます。例えば、`∃n∈N.P(n)`という自然数に関する命題は、P(0), P(1), P(2), ... を選言で繋いだ P(0)∨P(1)∨P(2)∨ ... と同じです。ということは、無限個の証明要求を作って無限の下請け業者に発注して、どれでもいいから納品があるのを待つことになります。

では、実数に関する命題`∃x∈R.P(x)`がターゲットならどうでしょうか。連続無限個の証明要求を作って連続無限の下請け業者に発注します。でも、連続無限個の証明要求って、具体的にどうやって書き上げるのでしょうか？ お膳立ての段階で、神様の（超越的な）能力が要求されます。

という事情で、ターゲットが存在命題`∃x∈X.P(x)`であるときのお膳立ては困難です。無限個の証明要求に書き換えるよりは、存在命題を同値な命題に置き換えたり、Xの具体的要素を表す項tをなんとか探し出して、P(t)を証明することになるでしょう。

[追記]
証明要求 Γ/ Δ |-? P∨Q を2つに分解して、どちらかの（どっちでもいい）証明を要求することが悪いわけではありません。が、他の書き換えのほうが適切な場合もあります。例えば、ターゲットを二重否定してみます。≡はメタな意味の同値性を表す記号として：

• P∨Q ≡ ¬¬(P∨Q) ≡ ¬(¬P∧¬Q)

背理法を使うことにすれば：

  Γ/ Δ |-? P∨Q
 -------------------------[同値]
  Γ/ Δ |-? ¬(¬P∧¬Q)
 -------------------------[背理法]
  Γ/ Δ, ¬P, ¬Q |-? ⊥

うまく矛盾が導き出せれば、もとの証明要求に応えたことになります。

[さらに追記]「証明の“お膳立て”のやり方 4： 随伴による集合差の定義」でさらに詳しい話をしています。[/さらに追記]
[/追記]

定義と補題の利用

「証明の“お膳立て”のやり方」の具体例で、次のような“お膳立て済みの証明要求”が登場しました。

• Γ/ `f<sup>*</sup>:Pow(B)→Pow(A)`, `f:A→B は全射ではない` |-? `∃S, T∈Pow(B).(f<sup>*</sup>(S) = f<sup>*</sup>(T) ∧ S ≠ T)`

ターゲットが存在命題なので、実例を作るしかありません。Im(f)はfの像集合として、S = Im(f), T = B と置くと適切な実例になります。しかし、Im(f)の定義が文脈知識Γにないとしたら、Im(f)という記号を使うことは契約違反になります。思い出してください。

• 納品された証明のなかに、顧客が解釈できない部分／許容できない部分があれば、契約違反となる。

未知の記号Imは、顧客が解釈できないものです。こんなときは、新しい記号（概念）の定義を、文脈知識か仮定に追加します。次のような命題を追加すればいいでしょう。

• ∀y∈B.(y∈Im(f) ⇔ ∃x∈A.(y = f(x)))

Imに関連する次の命題も前提に入れたいですね。

• fは全射 ⇔ Im(f) = B

これらを文脈知識に入れた証明要求は次のようになります。

• Γ, `∀y∈B.(y∈Im(f) ⇔ ∃x∈A.(y = f(x)))`, `fは全射 ⇔ Im(f) = B`/ `f<sup>*</sup>:Pow(B)→Pow(A)`, `f:A→B は全射ではない` |-? `∃S, T∈Pow(B).(f<sup>*</sup>(S) = f<sup>*</sup>(T) ∧ S ≠ T)`

イヤッ、ちょっと待って下さい。契約履行の基準のなかに次があります。

• ΓにもΔにも入ってない命題が仮定として使われたなら、契約違反となる。

`∀y∈B.(y∈Im(f) ⇔ ∃x∈A.(y = f(x)))`, `fは全射 ⇔ Im(f) = B` は、もとの前提（文脈または仮定）に入ってません。それを証明内で使えば、契約違反となるのではないでしょうか。

実は大丈夫です。契約違反として禁止されている行為は、無根拠に勝手に前提を増やしてしまうことです。すぐ上で行った行為は、証明作業の中間段階で定義や補題を利用してるだけです。もともと指定された前提を勝手に増やしてはいません。

この事情は、証明可能性判断と証明要求を一緒に使って説明できます。

  Γ/ Δ |-? Q   Γ/ Δ |- R
 -----------------------------[定義・補題の追加]
      Γ/ Δ, R |-? Q

顧客・元請け・下請けモデルで考えると分かりやすいです。上段左がもとの証明要求です。元請けが作業をして、Rの証明は出来上がっています（上段右）。元請けによる作業結果を前提に追加して、下請けに出す新しい証明要求を作ります。それが下段です。下段の証明要求に応える証明（＝成果物＝納品物）が下請けから上がってくれば、元請けは契約違反することなく顧客に納品できます。

つまり、前提が増えているのは元請けから下請けへの証明要求でのことで、増やした理由は Γ/ Δ |- R という証明が既にあるからです。勝手に増やしてはいません。定義の導入には特に前提を必要としないので、これももとの前提を勝手に増やしたことにはなりません。

ターゲットの取り替え

顧客と業者のあいだの契約上の禁止事項に次のものがありました。

• 証明要求で指定されたターゲットとは異なる命題が結論になっていれば、契約違反となる。

これは当たり前で、要求と異なる事をやっても認められません。しかし、元請け・下請けのあいだでは証明要求のターゲットを書き換えることはあります。

  Γ/ Δ |-? Q   Γ/ Δ |- R⇒Q
 -------------------------------[ターゲットの取り替え]
      Γ/ Δ |-? R

分かりますよね。元請け側で`R⇒Q`の証明を済ましている（上段右）ので、下請けに出す証明要求（下段）ではRをターゲットにしているのです。下請けからRの証明が上がってくれば、元請けがQの証明を作って納品することは容易です。契約違反は犯してません。

まとめ

メイヤー先生にならい、証明も顧客・業者モデルで考えることにしました。“お膳立て＝証明要求の書き換え”は、元請けが下請けに発注するときに新しい証明要求を作る作業に喩えることができます。

証明要求のターゲットが選言（∨）と存在（∃）を持つとき、それを取り除いて下請けに発注することは難しいです。それ以外の場合、∧, ⇒, ∀, ¬を取り除いて下請けに発注する方法、それと一部の証明を元請け側でやってから下請けに発注する方法を以下に並べます。

      Γ/ Δ |-? P∧Q
 ------------------------------[連言の分解]
  Γ/ Δ |-? P   Γ/ Δ |-? Q

  Γ/ Δ |-? P⇒Q
 ------------------[含意の変形]
  Γ/ Δ, P |-? Q

  Γ/ Δ |-? ∀x∈X.Q
 ----------------------[全称の変形]
  Γ/ Δ, x : X |-? Q

  Γ/ Δ |-? ¬Q
 -------------------[背理法]
  Γ/ Δ, Q |-? ⊥

  Γ/ Δ |-? Q   Γ/ Δ |- R
 -----------------------------[定義・補題の追加]
      Γ/ Δ, R |-? Q

  Γ/ Δ |-? Q   Γ/ Δ |- R⇒Q
 -------------------------------[ターゲットの取り替え]
       Γ/ Δ |-? R

元請けから下請けに回る段階で、もとの要求より易しい要求になっている点に注意してください。実に良心的な下請け構造なのです。

これは、元請けが“お膳立て＝証明要求の書き換え”を適切に行えば、下請けの証明作業が必ず簡単になることを意味します。この比喩で、お膳立ての意義と重要性が分かるでしょう。

*1:現実世界では、無理難題を下請けに押し付けて、オイシイところだけは元請けで担当するなんてこともありそうです。