共有知識の論理

2000年 3月 29日

日本数学会 2000年度年会数学基礎論および歴史分科会

永島孝

無所属, 一橋大学名誉教授

                      nagasima-t@mta.biglobe.ne.jp
                   http://www2s.biglobe.ne.jp/~hotori/

共有知識を扱う新しい^{1} 述語論理系を提示する. Kaneko and Nagashima の Game logic GL_{ω} では多様相述語論理を無限論理へ拡張し無限個の式に対しても ∧, ∨ が適用できるようにした. これに対して, ここに新たに提示する論理系は finitary ではないけれども, 無限に長い式をもちいず, 推論規則のうち一つだけについて無限個の前提を許すものである.

共有知識の命題論理としては Halpern and Moses の体系が知られている. これは共有知識を不動点として定める推論規則のある finitary な体系である.

一方, 共有知識の述語論理は recursively enumerable でないことを Frank Wolter が証明した. 従って, 共有知識の (完全な) 述語論理系は finitary には作り得ない.

共有知識とは?

様相記号_{1}, …, _{n} のある多様相論理を考える. n 人の人がいるとして, _{i}A は人 i が A を知っている ( K_{i}A) または信じている ( B_{i}A) ことをあらわす.

A がその n 人の間の共有知識であるとは,

i_{1} _{i_{2}}… _{i_{k}}A

があらゆる有限列 i_{1}i_{2} … i_{k} ∈ {1,…, n}^{∗} についてなりたつことをいう. これを CA であらわす.

(注. i_{1} ≠ i_{2} ≠ ⋯ ≠ i_{k} という制限を設ける場合もある. たとえば GL_{ω} ではこの立場を採用した.)

GL_{ω} では CA を_{i_{1}} _{i_{2}}… _{i_{k}}A の形の式の全体の conjunction の省略形と考えた. これに反して, ここに提示する新しい体系では共有知識記号 C を基本記号の一つとして採用し, これに関する推論規則を多様相述語論理に追加する.

困難は?

古典命題論理につぎのものを添加して拡張すると考える.

(1) quantifiers ∀, ∃.

(2) 様相_{1}, …, _{n}.

(3) 共有知識 C.

1 2000 年 4 月 20 日追記. 新しいのは (→ C) の推論規則についての田中義人氏の創案と完全性の証明であり, 田中氏による改良の前の体系については永島が過去の研究会等で発表してきましたが, 同等の体系がそれ以前からすでに知られていたことがわかりました. また, 後述の定理 1–10 のうちのいくつかも知られていた可能性もあります. したがって永島の関与したと現時点で考えられるのは (→ ∀) の推論規則を変えて Barcan 公理を吸収させることと, 定理のなりたつのを確認したことのみにとどまります. また, Wolter の結果に関しては鈴木信行氏のご教示によります.

(1) と (2) では多様相述語論理, (1) と (3) では様相述語論理 S4 にあたるもの, そして (2) と (3) では共有知識の命題論理になり, いずれも finitary な形式的体系が知られている. これに反して (1), (2), (3) を同時に添加しようとすると finitary にはできないというのが Wolter の定理の帰結である. 三つを同時に添加するときに限り finitary になり得ないという不思議な現象から, Halpern and Moses の共有知識の命題論理の体系に quantifier rules をつけ加えたのは何になるのかという謎が生まれる.

記号と推論規則

記号. 自由変数 a_{0} , a_{1} , … (可算無限個). 束縛変数 x_{0} , x_{1} , … (可算無限個). 述語記号 (1 個以上). 論理記号 ¬, ⊃, ∧, ∨, ∀, ∃. 様相記号_{1}, …, _{n}. 共有知識記号 C.

式 (formula) も sequent も通常のとおり有限的に構成する. 推論規則. まず, 古典述語論理 LK を多様相述語論理に拡張する. 推論規則

{Γ, _{i}Δ ⟶ Θ \atop _{i}Γ, _{i}Δ ⟶ _{i}Θ} ( _{i})  ただし|Θ| ≤ 1

を各 i について添加した多様相述語論理 KD4_{n} を想定しているけれども, K_{n} , S4_{n} などでも共有知識の論理への拡張は同様にできる. なお, いずれの様相論理をもとにする場合も Barcan formula に相当する sequent

∀x _{i}A ⟶ _{i}∀x A

を initial sequent として採用する. なお, これについては後でふたたび述べる.

e = i_{1}i_{2} … i_{k} ∈ {1,…, n}^{∗} に対して_{i_{1}} _{i_{2}}… _{i_{k}}A を_{e}A と略記する. とくに k = 0 の場合すなわち e が空列の場合には_{e}A は A である.

共有知識に関する推論規則など

∧ の推論と同様に考えて, まず (C →) は

{_{e}A, Γ ⟶ Θ \atop CA, Γ ⟶ Θ}  ただしe ∈ \{1,…, n\}^{∗}

とする. つぎに (→ C) も同様に考えて

{Γ ⟶ Θ, _{e}A | e ∈ {1,…, n}^{∗}} ; Γ ⟶ Θ, CA

を試みたけれども, これでは十分でない.

Y. Tanaka は (→ C) をつぎの形にすることで Kripke 完全性の得られることを示した.

{Γ ⟶ Θ, _{i_{1}}(D_{1} ⊃ _{i_{2}}(D_{2} ⊃ ⋯ _{i_{m}}(D_{m} ⊃ _{e}A) · ·)) | e ∈ {1,…, n}^{∗}} ; Γ ⟶ Θ, _{i_{1}}(D_{1} ⊃ _{i_{2}}(D_{2} ⊃ ⋯ _{i_{m}}(D_{m} ⊃ CA) · ·))

( m は任意の自然数; i_{1} , i_{2} , …, i_{m} ∈ {1,…, n}; D_{1} , D_{2} , …, D_{m} は任意の式. m = 0 の場合がもとの形に相当する.)

この体系の infinitary なのは推論 (→ C) の upper sequents が無限個あるというところだけである.

さて, (→ C) にならって (→ ∀) も LK でのもとの形

{Γ ⟶ Θ, A[a/x] \atop Γ ⟶ Θ, ∀x A}

から一般化して

{Γ ⟶ Θ, _{i_{1}}(D_{1} ⊃ _{i_{2}}(D_{2} ⊃ ⋯ _{i_{m}}(D_{m} ⊃ A[a/x]) · ·)) \atop Γ ⟶ Θ, _{i_{1}}(D_{1} ⊃ _{i_{2}}(D_{2} ⊃ ⋯ _{i_{m}}(D_{m} ⊃ ∀x A) · ·))}

とする. 変数条件は LK と同様, eigenvariable a は lower sequent に含まれないとする. この形にすると Barcan sequent を initial sequent とすることなく Barcan formula が証明される.

わかったことなど

注. ∗ 印の定理は, モデルをもちいれば証明できるけれども, 証明論的には未解決である.

定理 1. [Barcan formula] ⊢ ∀x _{i}A ⊃ _{i}∀x A. 定理 2. [Barcan formula for C] ⊢ ∀x CA ⊃ C∀x A. 定理 3. [Conservativeness] 式 A が様相記号_{1}, …, _{n}, C をいずれも含まないとき, ⊢ A であるためには A が古典述語論理で証明可能であることが必要十分. 定理* 4. [Conservativeness] 式 A が記号 C を含まないとき, ⊢ A であるためには A が多様相述語論理 KD4_{n} + BF で証明可能であることが必要十分. 定理 5. 式 A が記号_{1}, …, _{n} をいずれも含まないとして, A に現れる記号 C をすべてに書き替えたものを A′ とすると, ⊢ A であるためには A′ が様相述語論理 S4 + BF で証明可能であることが必要十分. 定理* 6. [Conservativeness] A が quantifier を含まず ⊢ A ならば, A の証明図で quantifier rules を含まないものがある. 定理 7. [Fixed point] ⊢ CA ≡ A ∧ C _{1}A ∧… ∧ C _{n}A. 定理 8. [Fixed point] ⊢ CA ≡ A ∧ _{1}CA ∧… ∧ _{n}CA. 定理 9. ⊢ B ⊃ A ∧ _{1}B ∧… _{n}B ならば ⊢ B ⊃ CA. 定理 10. この体系で証明可能な式は GL_{ω} で証明可能である. 予想. GL_{ω} で証明可能な式で infinitary な ∨ を含まず C( · ) の形以外に infinitary な ∧ を含まないものはこの体系で証明可能. 予想. 証明可能な式 A が記号 C を positive に含まないとき, A の証明図で推論 (→ C) を含まないものがある.

(以上)