このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

シーケントに親しもう (A11P9)

RSS練習問題

※この記事は「記事11 問題集9」

記号的表現に対して「自然言語（日本語や英語）による読み下しが出来ないと馴染めない」という事情も当然だから、シーケントの読み下し練習をする。そして、「“シーケントの正しさ”を正しく判断する／判断できる」とはどういうことか？ を（できれば）納得して欲しい。問題を解きながらストーリーを追い、出来るだけリアルにシリアスに状況をイメージしてくださいな。

他の練習問題をする前に、この記事をザッと読んだほうがいいかも知れない。
[追記]続きの記事があります。

[/追記]

内容：

  1. ゲンツェンのLKシーケント計算をご存知の方への注意
  2. シーケントを読み下そう
  3. 疑問文を作ろう
  4. その疑問文に、誰がどのように答えるのか？
  5. 演繹システムの格付け作業はどう行うか？

ゲンツェンのLKシーケント計算をご存知の方への注意

検索などでたまたまここに辿り着いた人が誤解するのも困るので、毎回この節を冒頭に置くことにする。

  1. '⇒'は含意〈条件法〉の論理結合子で、'→'がシーケントの左右を区切る記号である。
  2. ゲンツェンのLKシーケントでは、左辺のカンマは連言的に、右辺のカンマは選言的に解釈をする。ここでのシーケントでは、出現位置の情報を使わずに、カンマは常に連言的であり、選言的な区切り記号に縦棒'|'を使う。
  3. (x∈R, n∈N) のような書き方は、集合論の命題ではなくて、自由変数の型宣言（のリスト）である。自由変数の型宣言のリストをコンテキストと呼ぶ。
  4. 暗黙のコンテキストを使う場合もあるが、できるだけ、シーケント内に明示的にコンテキストを書き込むようにしている。

シーケントを読み下そう

左辺が連言的リストで右辺が唯一つの論理式からなるシーケントだけを扱う。この形だけでも実用性は十分にある。この種のシーケントの形は、α1, ..., αn をコンテキスト、Γ1, ..., Γn を連言的リストとして、

  • α1, Γ1, ..., αn, Γn → B

例えば、

  • (n∈N), ∃k∈N.(n = 2k), n ≦ 10, (a∈R), (x∈R), T → ∃y∈R.(yn = a2)

この例では：

  1. コンテキスト α1 に相当するのは、コンテキスト (n∈N)
  2. 連言的リスト Γ1 に相当するのは、連言的リスト ∧(∃k∈N.(n = 2k), n ≦ 10)
  3. コンテキスト α2 に相当するのは、コンテキスト (a∈R)
  4. 連言的リスト Γ2 に相当するのは、空な連言的リスト ∧()
  5. コンテキスト α3 に相当するのは、コンテキスト (x∈R)
  6. 連言的リスト Γ3 に相当するのは、（長さが1の）連言的リスト ∧(T)
  7. 命題 B に相当するのは、命題 ∃y∈R.(yn = a2)

冒頭に書いた制限「左辺が連言的リストで右辺が唯一つの論理式からなるシーケントだけを扱う」から、リストは常に連言的なので、単にリストと書いたら連言的リストとする。つまり、カンマは論理ANDと解釈してよい。

シーケントを、英語ベースの自然言語風の書き方にするルールは：

  1. コンテキストの前に For を付ける。
  2. 左辺に登場する論理式のリストの前に Given を付ける。
  3. 矢印の代わりに Holds で区切る。
  4. 右辺の論理式を書いて、End で終わる。
  5. 空コンテキストや空リストに関する記述は省略してよい。



For α1

Given Γ1

 …

For αn

Given Γn

Holds

  B

End

実例：



For n∈N

Given ∃k∈N.(n = 2k), n ≦ 10

For a∈R

For x∈R

Given T

Holds

 ∃y∈R.(yn = a2)

End

シーケントを、日本語ベースの自然言語風の書き方にするルールは：

  1. コンテキストは、「型 変数名 に対して、」と書く。変数が複数あるときは、「型1 変数名1 と 型2 変数名2 に対して、」のように「と」で繋ぐ。
  2. 左辺に登場する論理式のリストの後に 「だとする。」を付ける。
  3. 矢印の代わりに 「これらより、」で区切る。「ら」が不自然なときは「これより、」でもよい。
  4. 右辺の論理式を書いて、「が出る。」 で終わる。
  5. 空コンテキストトや空リストに関する記述は省略してよい。



自然数 n に対して、

∃k∈N.(n = 2k), n ≦ 10 だとする。

実数 a に対して、

実数 x に対して、

T だとする。

これらより、

 ∃y∈R.(yn = a2)

が出る。

英語風／日本語風に書いたシーケントが内容的に正しいか正しくないかはとりあえず置いといて、形としては、定理のステートメント〈主張〉のように読めるだろう。

問題： 以下にあげるシーケントに対して、α1, Γ1, ..., αn, Γn, B に相当する部分がどんなコンテキスト、リスト、論理式であるかを明確にせよ（先の例のように）。
問題： 以下にあげるシーケントを、英語ベースの自然言語風の書き方に直せ。英語として多少不自然になるのは致し方ない。
問題： 以下にあげるシーケントを、日本語ベースの自然言語風の書き方に直せ。日本語として多少不自然になるのは致し方ない。

シーケント：

  1. (x∈R, y∈R), x ≧ 0, y ≧ 0 → x + y ≧ 0
  2. (x∈R, y∈R), x ≧ 0, y ≦ 0, (n∈N), T → xn + yn ≧ 0
  3. (x∈R, y∈R), (n∈N) → xn + yn ≧ 0
  4. (x∈R, y∈R), x ≧ 0, y ≦ 0, (n∈N), ∃k∈N.(n = 2k) → xn + yn ≧ 0
  5. (x∈R, y∈R), (n∈N), ∃k∈N.(n = 2k) → xn + yn ≧ 0
  6. (x∈R, y∈R, n∈N), ∃k∈N.(n = 2k) → xn + yn ≧ 0
  7. (x∈R, y∈R, n∈N) → ∃k∈N.(n = 2k) ⇒ xn + yn ≧ 0
  8. (x∈R, y∈R) → ∀n∈N.(∃k∈N.(n = 2k) ⇒ xn + yn ≧ 0)

疑問文を作ろう

Aが命題のとき、「Aは正しいか？」という疑問文は意味を持つ。シーケントは、定理のステートメントを形式化したものと考えよう。すると、シーケントψに対して「ψは正しいか？」という疑問文も意味を持つだろう -- 誰かが、ψ（で表現される）ステートメントを主張したとき、「彼の主張は正しいか？」という疑問文は意味を持つのだから。

この状況にリアリティを持たせるために、シーケントが正しいかどうかを問う疑問文を実際に作ってみる。

英語風：

  1. 英語ベースの自然言語風の書き方の場合は、シーケント（の英語風表現）全体を引用符で囲む。
  2. Is "……" correct? という疑問文を作る。

日本語風：

  1. 日本語ベースの自然言語風の書き方の場合は、シーケント（の日本語風表現）全体を鉤括弧で囲む。
  2. 「……」は正しいか？ という疑問文を作る。

例：



英語風：

Is "For n∈N Given ∃k∈N.(n = 2k), n ≦ 10 For a∈R For x∈R Given T Holds  ∃y∈R.(yn = a2) End" correct?



日本語風：

「自然数 n に対して、∃k∈N.(n = 2k), n ≦ 10 だとする。実数 a に対して、実数 x に対して、T だとする。これらより、 ∃y∈R.(yn = a2) が出る。」は正しいか？

問題: 前節の8個のシーケントに対して、そのシーケントは正しいか？ という疑問文を英語風／日本語風で作成せよ。

その疑問文に、誰がどのように答えるのか？

コンテキストは α, β など、単一の論理式は A, B など、論理式のリスト（ここでは連言的リスト）は Γ〈大文字ガンマ〉, Δ〈大文字デルタ〉などで表す。シーケントは小文字ギリシャ文字の後のほう、ψ〈小文字プサイ〉, φ〈小文字ファイ〉 などを使う。ふー、文字種が足りない。

シーケントψが与えられたとき、「ψは正しいか？」という疑問文に誰が答えるかに関して、ニ通りのケースを想定する。

  • ケース1: 我々、現実世界に生きている人間、私（檜山）やあなたが答える。
  • ケース2: ソフトウェアシステムが答える。

ケース2、ソフトウェアシステム（架空のものかも知れない）に答えさせることを考える。シーケント（のデータ）を入力すると、それが正しいかどうかを判断して答えるソフトウェアシステムが10種あるとする。それぞれ S1, S2, ..., S10 とする。

ソフトウェアシステムに入力するために、1000個のシーケントを準備する。ψ1, ψ2, ..., ψ1000 としよう。

ソフトウェアシステムの優劣を格付けするために次の基準を設ける。

  1. 1000個のシーケントすべての正しさを正しく判定した場合は「優」ランクとする。
  2. 1000個のシーケントのうち950個以上の正しさを正しく判定した場合は「良」ランクとする。
  3. 1000個のシーケントのうち800個以上の正しさを正しく判定した場合は「可」ランクとする。
  4. 1000個のシーケントのうち800個未満の正しさしか正しく判定できなかった場合は「不可」ランクとする。

ソフトウェアシステムではなくて、中にいる小人さんや妖精さんが答えてくれるシステムでもかまわない。要は、現実世界に生きて暮らしている我々人間以外が判断主体となる人工的または仮想的（おとぎ話的）なシステムならよい。

演繹システムの格付け作業はどう行うか？

10個の演繹システム（ソフトウェアシステム、または小人さん・妖精さんの世界）S1, S2, ..., S10 を格付けしよう。もし「優」ランクのシステムがあれば、それは実用に耐えるだろう。「良」ランクでも使えなくはない（けっこう間違うが）。「可」でもいい人がいるかも知れない。「不可」は間違えすぎだ。

格付けのテストが終わると（終わればね）、例えば（例えばね）次のような結果が出るかもしれない。

  • S1 不可
  • S2 可
  • S3 不可
  • S4 良
  • S5 不可
  • S6 不可
  • S7 不可
  • S8 優
  • S9 可
  • S10 不可

演繹システム達が出す結果を我々人間が評価するためには、事前に1000個のシーケントの正しさを我々人間が知っていなくてはならない。そうでないなら格付けできない。ここで、ケース1がどうしても必要になる。

  • ケース1: 我々、現実世界に生きている人間、私（檜山）やあなたが答える。

次の1000個の疑問文に、現実世界に生きている我々人間が先に答えを出しておく必要がある。

  • Is "ψ1" correct?
  • Is "ψ2" correct?
  • Is "ψ3" correct?
  • ...
  • Is "ψ999" correct?
  • Is "ψ1000" correct?

現実世界に生きている我々人間が判断する方法とは、つまり、いつもどおりに普通に数学を使って判断することである。集合やら写像やらをいつもどおりに普通に利用して考えるだろう。霊感に頼ったり、サイコロを振っては決めないはず。

人工的または仮想的な演繹システムを調べる前に、「シーケントの正しさ」という概念を、現実世界に生きている我々人間が雰囲気ではなく確実に理解できる形で普通に定義しておく必要がある。演繹システム達は我々の評価（格付け）の対象であり、事前に信用できる保証など何もない。だから、次の“普通の定義”がある。

  • シーケントψが正しい とは ψのスコット・ブラケット（の値）〚ψ〛が、ψのコンテキストαの領域 Dom(α) と一致することである。

ここで出てくるスコット・ブラケットは、特殊な括弧記号を使っているが、普通の方法で定義可能な関数である。例えば、Scottのような関数名を使ってもよい（凹レンズ括弧を使うのは単なる習慣だから）。

スコット・ブラケット、あるいは関数Scottの定義は以下のとおりである。

与えられたシーケントψのコンテキストを左端にまとめる（シーケントの正規化）。まとめた後のψ'は

  • α, Γ → B

という形にできる。αはコンテキスト、Γは論理式のリスト、Bは論理式である。与えられたシーケントψ、正規化されたシーケントψ'に対して、

  • Scott(ψ) := Scott(ψ')
  • Scott(ψ') = 〚ψ'〛 = 〚α, Γ → B〛 := 〚α| Γ〛c ∪〚α| B〛

ここで：

  1. ψ'は α, Γ → B という正規化後のシーケントのこと。
  2. Scottはスコット・ブラケットの関数名
  3. 〚α| Γ〛は、コンテキストαのもとでの論理式のリストΓのスコット・ブラケット
  4. 右肩のcは部分集合の補集合をとる集合演算
  5. ∪は、部分集合の合併をとる集合演算
  6. 〚α| B〛は、コンテキストαのもとでの論理式Bのスコット・ブラケット

上の定義内で論理式のリストに対するスコット・ブラケットが必要になるが：

  • 〚α| Γ〛 = 〚α| A1, ..., An〛 := 〚α| A1〛∩ ... ∩〚An〛

ここで：

  1. 〚α| A1〛は、コンテキストαのもとでの論理式A1のスコット・ブラケット
  2. 〚α| An〛は、コンテキストαのもとでの論理式Anのスコット・ブラケット。その他も同じ。
  3. ∩は、部分集合の共通部分をとる集合演算

結局、単一の論理式に対するスコット・ブラケットに帰着される。その基本的な場合のスコット・ブラケットは、

リンク先の問題を解くときは、経験と直感に頼ってもよい。が、単一の論理式に対するスコット・ブラケットの定義を、普通の数学内で厳密に書くことができる（「正しさ」「正しさの程度」を哲学的・理念的に語ったりはしない！）。

スコット・ブラケットという関数の定義が厳密に書けることと、その関数がアルゴリズム的に計算可能なことは別問題である。数学における関数の定義は、計算手順を伴うわけではないから。

また、格付けテスト用のデータである ψ1, ψ2, ..., ψ1000 は、我々人間が事前に正しいかどうかを確認済みでないと格付けテストに使えないが、全く勝手に与えられたシーケント φ に対して、正しいかどうかを常に我々が判定できるとは言ってない。

  • 我々人間と同じ能力を持つシステムSがあれば、Sは「優」ランクとなる。
  • 我々人間と同じ能力を持つシステムSがあれば、テストに使うシーケント数がいくら増えても、常に人間と同じ答えを出す（はず）。
  • 我々人間と同じ能力を持つ（と想定される）システムSは、事前に我々人間が確認してないシーケントφを勝手に与えられたとき、シーケントφが正しいかどうかを常に判定できるのだろうか？
  • 我々人間と同じ能力を持つ（と想定される）システムSが、勝手に与えられたシーケントψが正しいかどうかを常に判定できるのなら、我々人間もまた、勝手に与えられたシーケントが正しいかどうか判定できることになる。Sに出来て人間に出来ないはずはない。

[追記]続きの記事があります。

[/追記]