共有知識の論理について

(On a System of Common Knowledge Logic)

短期共同研究 “認識論理とゲーム理論” (代表者金子守) 1999年 8月 30日–9月 1日, 京都大学数理解析研究所 (August 30–September 1, 1999, RIMS, Kyoto) 1999年 9月 1日に発表したときの配付資料を 1999年 9月 6日に改訂 Setember 1, revised September 6, 1999

永島孝 (Nagashima Takashi) 無所属, 一橋大学名誉教授 (Emeritus Professor of Hitotsubashi University) Email address (see my website)

                  Web site http://www2s.biglobe.ne.jp/~hotori/

序

ゲームのプレーヤーが n 人いるとして, それらのプレーヤーの共有知識 (common knowledge) の記述のために, まず各プレーヤーに対してプレーヤー i の知識 (knowledge) あるいは信念 (belief) をあらわす様相演算子 K_{i} を古典述語論理の体系に追加する. 式 A であらわされる命題に対して, A であることを第 iプレーヤーが知っている (あるいは信じている) のを K_{i}A であらわすとする. A が共有知識であるとは, n = 2 の場合を例示すれば,

A, K_{1}A, K_{2}K_{1}A, K_{1}K_{2}K_{1}A, … K_{2}A, K_{1}K_{2}A, K_{2}K_{1}K_{2}A, …

がすべてなりたつことをいう. A が共有知識であることを CA と記す.

金子・永島の Game Logic GL_{ω} [KN96] では無限個の式に対しても ∧ が適用できるように多様相述語論理 KD4 の体系を infinitary logic に拡張し, CA を式 A ∧ K_{1}A ∧ K_{2}A ∧ K_{2}K_{1}A ∧ K_{1}K_{2}A ∧ K_{1}K_{2}K_{1}A ∧ … の省略と考える.

さて, 無限論理 (infinitary logic) を扱うことに伴う困難をなるべく少なくするために, formula や sequent は有限で, 推論規則の一つにだけ無限個の前提を認める体系を考え, CK と名付ける.^{1} この体系 CK について, 証明論の立場から基本的な事実をあきらかにし, GL_{ω} や Halpern and Moses の体系との比較などを考察する. いままで GL_{ω} で扱ってきた問題はおおむね新しい体系 CK でも扱えるであろうと思われる.

まず共有知識を表す C を基本記号の一つとするのが, 体系 CK の GL_{ω} とのちがいである.

共有知識の体系 CK について

以下, プレーヤーの人数を表す任意の正の整数 n を固定して考える. 記号はつぎのとおり. 自由変数 a_{0} , a_{1} , … (可算無限個). 束縛変数 x_{0} , x_{1} , … (可算無限個). 定数記号および函数記号. 述語記号 (1 個以上).

1[K99] には CK に似た命題論理の体系 CKL(G) がある.

論理記号 ¬, ⊃, ∧, ∨, ∀, ∃. 知識記号 K_{1} , …, K_{n} , C .

式 (formula) の構成は古典述語論理におけるのと同様にし, つぎの二つの項目を追加する. A が式ならば K_{i}A は式である. A が式ならば CA は式である. 古典述語論理におけるのとおなじく, Γ と Θ とがおのおの式の有限列であるとき Γ ⟶ Θ は

sequent であると定める.

Formula A が証明可能であるとは, sequent ⟶ A が証明可能であることと定義する.

Barcan axiom を含む KD4 の多様相述語論理 KD4_{n} をまず考え, これに C に関する公理と推論規則とを追加する. なお, KD4 以外の様相述語論理についても, Barcan axiom をみたす normal な様相論理については同様な拡張が考えられるであろう.

第一階古典述語論理 LK をまず考え, これを Barcan axiom を含む多様相述語論理 KD4_{n} に拡張し, これに C に関する公理と推論規則とをさらに追加する.

まず古典述語論理の体系 LK はつぎのとおりである.

Initial Sequent: A ⟶ A 推論規則:

{Γ ⟶ Θ \atop A, Γ ⟶ Θ} (t →)  {Γ ⟶ Θ \atop Γ ⟶ Θ, A} (→ t)
{A, A, Γ ⟶ Θ \atop A, Γ ⟶ Θ} (c →)  {Γ ⟶ Θ, A, A \atop Γ ⟶ Θ, A} (→ c)
{Γ, A, B, Δ ⟶ Θ \atop Γ, B, A, Δ ⟶ Θ} (i →)  {Γ ⟶ Θ, A, B, Λ \atop Γ ⟶ Θ, B, A, Λ} (→ i)
\begin{matrix}Γ ⟶ Θ, A & A, Δ ⟶ Λ \\ Γ, Δ ⟶ Θ, Λ \end{matrix} (cut)
{Γ ⟶ Θ, A \atop ¬A, Γ ⟶ Θ} (¬ →)  {A, Γ ⟶ Θ \atop Γ ⟶ Θ, ¬A} (→ ¬)
\begin{matrix}Γ ⟶ Θ, A & B, Δ ⟶ Λ \\ A ⊃ B, Γ, Δ ⟶ Θ, Λ \end{matrix} (⊃ →)  {A, Γ ⟶ Θ, B \atop Γ ⟶ Θ, A ⊃ B} (→ ⊃)
\begin{matrix}{B, Γ ⟶ Θ \atop A ∧ B, Γ ⟶ Θ} & (∧ →) \\ {A, Γ ⟶ Θ \atop A ∧ B, Γ ⟶ Θ} & (∧ →) \end{matrix}  \begin{matrix}Γ ⟶ Θ, A & Γ ⟶ Θ, B \\ Γ ⟶ Θ, A ∧ B \end{matrix} (→ ∧)

\begin{matrix}A, Γ ⟶ Θ & B, Γ ⟶ Θ \\ A ∨ B, Γ ⟶ Θ \end{matrix} (∨ →)  \begin{matrix}{Γ ⟶ Θ, A \atop Γ ⟶ Θ, A ∨ B} & (→ ∨) \\ {Γ ⟶ Θ, B \atop Γ ⟶ Θ, A ∨ B} & (→ ∨) \end{matrix}

{F (t), Γ ⟶ Θ \atop ∀x F (x), Γ ⟶ Θ} (∀ →)  {Γ ⟶ Θ, F (a) \atop Γ ⟶ Θ, ∀x F (x)} (→ ∀)
{F (a), Γ ⟶ Θ \atop ∃x F (x), Γ ⟶ Θ} (∃ →)  {Γ ⟶ Θ, F (t) \atop Γ ⟶ Θ, ∃x F (x)} (→ ∃)

条件. 推論規則 (→ ∀) , (∃ →) において自由変数 a は Γ , Θ にも F (x) にも含まれないとする.

ここまでが第一階古典述語論理 LK である. つぎに N := {1, …, n} として, K_{i} ( i ∈ N ) に関する initial sequent と推論規則とを追加する.

∀x K_{i}F (x) ⟶ K_{i}∀x F (x) (B) (i ∈ N)

{Γ, K_{i}Δ ⟶ Θ \atop K_{i}Γ, K_{i}Δ ⟶ K_{i}Θ} (K → K)  (i ∈ N)

条件. 推論規則 (K → K) において Θ はたかだか一個の式を含むとする.

ここまでが多様相述語論理 KD4_{n} である. つぎに C に関する規則を導入する準備としてつぎのとおり定める. N^{⟨ω⟩} = {(i_{1}, …, i_{m}) | m ≥ 0, i_{1} ≠ i_{2} ≠ … ≠ i_{m}} とおき, N^{⟨ω⟩} ∋ e = (i_{1}, …, i_{m}) に対して e の長さ m を |e| で表し, K_{i_{1}} ⋯ K_{i_{m}} を省略して K_{e} と書く. さらに演算 ∗: N^{⟨ω⟩} × N^{⟨ω⟩} → N^{⟨ω⟩} を e = (i_{1}, …, i_{m}) , e′ = (j_{1}, j_{2}, …, j_{l}) のとき

e ∗ e′ = \{ \begin{matrix}e & if l = 0, \\ e′ & if m = 0, \\ (i_{1}, …, i_{m}, j_{2}, …, j_{l}) & if m > 0, l > 0 and i_{m} = j_{1}, \\ (i_{1}, …, i_{m}, j_{1}, j_{2}, …, j_{l}) & if m > 0, l > 0 and i_{m} ≠ j_{1} \end{matrix}

であると定める. i ∈ N のとき (i) を略して i と書く.

C に関する initial sequent と推論規則とを追加する.

CA ⟶ K_{i}CA (CKC) (i ∈ N)

{K_{e}A, Γ ⟶ Θ \atop C(A), Γ ⟶ Θ} (C →) (e ∈ N^{⟨ω⟩})  \{Γ ⟶ Θ, K_{e}A | e ∈ N^{⟨ω⟩}\} ; Γ ⟶ Θ, C(A) (→ C)

以上の体系が, 共有知識の論理体系 CK である. この体系で infinitary なのは推論規則 (→ C) だけである.

問題 1. CK の意味論について. 補題 1. つぎの推論が CK で許容される. ただし |Θ| ≤ 1 .

{K_{e_{1}}A_{1}, …, K_{e_{m}}A_{m} ⟶ Θ \atop K_{e∗e_{1}}A_{1}, …, K_{e∗e_{m}}A_{m} ⟶ K_{e}Θ} .

補題 2. [Barcan rule for K_{e} ] ⊢CK ∀x K_{e}F (x) ⟶ K_{e}∀x F (x) . 証明.

\begin{matrix}∀x K_{1}K_{2}F (x) ⟶ K_{1}∀x K_{2}F (x) & {∀x K_{2}F (x) ⟶ K_{2}∀x F (x) \atop K_{1}∀x K_{2}F (x) ⟶ K_{1}K_{2}∀x F (x)} (K → K) \\ ∀x K_{1}K_{2}F (x) ⟶ K_{1}K_{2}∀x F (x) \end{matrix} ; (cut) ,

以下同様. 定理 3. [Barcan rule for C] ⊢CK ∀x CF (x) ⟶ C∀x F (x) . 証明. 補題 2 をもちいて, 各 e ∈ N^{⟨ω⟩} に対して

\begin{matrix}\begin{matrix}{K_{e}F (a) ⟶ K_{e}F (a) \atop CF (a) ⟶ K_{e}F (a)} & (C →) \\ ∀x CF (x) ⟶ K_{e}F (a) \end{matrix} ; (∀ →) ; ∀x CF (x) ⟶ ∀x K_{e}F (x) ; (→ ∀) & ∀x K_{e}F (x) ⟶ K_{e}∀x F (x) \\ ∀x CF (x) ⟶ K_{e}∀x F (x) \end{matrix} (cut)

ゆえに (→ C) をもちいて ∀x CF (x) ⟶ C∀x F (x) .

定理 4. [Conservativeness] A が知識記号 K_{1} , …, K_{n} , C をいずれも含まないとき ⊢CK A ⟺ ⊢LK A.

証明. [KN96] の Proposition 4.1 の証明と同様, 証明図の中の K_{1} , …, K_{n} , C をすべて消してしまう変換を考える. すなわち, 各 formula A に対して A^{ε} をつぎのとおり帰納的に定める. A が atomic ならば A^{ε} は A である. (A ⊃ B)^{ε} は A^{ε} ⊃ B^{ε} である. ¬, ∧, ∨ についても同様. (∀x F (x))^{ε} は ∀x F^{ε}(x) である. ∃ についても同様. (K_{i}A)^{ε} は A^{ε} である. (CA)^{ε} は A^{ε} である. CK における証明図の中の各 formula A を A^{ε} に置き換えた結果から LK における証明図が容

易に得られる. 逆はあきらか. 定理 5. [Conservativeness] A が記号 C を含まないとき ⊢CK A ⟺ ⊢_{KD4_{n}} A. 証明. (金子) C の K_{e} による有限近似を考える. 概略のみ述べる. 各自然数 m に対応して, 式を式に写す変換 ε^{m} , ε_{i}^{m} ( i ∈ N ) をつぎのとおり帰納的に定義する. A が atomic のとき, ε^{m}A も ε_{i}^{m}A も A である. ε^{m}(A ⊃ B) は ε^{m}A ⊃ ε^{m}B であり, ε_{i}^{m}(A ⊃ B) は ε_{i}^{m}A ⊃ ε_{i}^{m}B である. ¬, ∧, ∨, ∀, ∃ についても同様. ε^{0}K_{j}A, ε_{i}^{0}K_{j}A はいずれも ε^{0}A である. ε^{m+1}K_{i}A は ε_{i}^{m}A であり, ε_{i}^{m+1}K_{i}A は K_{i}ε_{i}^{m+1}A であり, ε_{i}^{m+1}K_{j}A ( i ≠ j ) は K_{j}ε_{j}^{m}A である. ε^{m}CA は ∧{ε^{m}K_{e}A | e ∈ N , |e| ≤ m} であり, ε_{i}^{m}CA は ∧{ε_{i}^{m}K_{e}A | e ∈ N , |e| ≤ m} である.

⊢CK A のとき, 十分大きい m をとれば ⊢_{KD4_{n}} ε^{m}A であることを示せばよい. 逆はあきらか. 定理 6. A が記号 K_{1} , …, K_{n} をいずれも含まないとき, A に現れる記号 C をすべてに書き替えたものを A′ とすれば ⊢CK A ⟺ ⊢S4 A′ . 証明. CK における証明図において K_{1} , …, K_{n} , C をすべてに書き替えた結果から S4 における証明図が容易に得られる. 逆は二つの推論規則

{A, Γ ⟶ Θ \atop CA, Γ ⟶ Θ}  {CΓ ⟶ A \atop CΓ ⟶ CA}

が CK において許容されることを示せばよい.^{2} 左は (C →) の特別の場合に過ぎない. 右は CΓ ⟶ A から任意の e ∈ N^{⟨ω⟩} に対して CΓ ⟶ K_{e}A の導かれることをつぎのように証明する. Γ を D_{1} , …, D_{k} として,

CD_{1} ⟶ K_{i}CD_{1}  {CD_{1}, CD_{2}, …, CD_{k} ⟶ A \atop K_{i}CD_{1}, K_{i}CD_{2}, …, K_{i}CD_{k} ⟶ K_{i}A} (K → K)

CD_{1}, K_{i}CD_{2}, …, K_{i}CD_{k} ⟶ K_{i}A (cut)

⋮ . CD_{1}, CD_{2}, …, CD_{k} ⟶ K_{i}A

以下同様に繰り返す. 定理 7. [Conservativeness] A が記号 ∀, ∃ を含まず ⊢CK A ならば, A は CK で (∀ →) , (→ ∀) , (∃ →) , (→ ∃) , (B) をもちいずに証明可能である. 証明. 簡単のため定数記号と函数記号とはないものとする. CK における任意の証明図 P を一つ固定して考える. 証明図 P に含まれる推論 (→ ∀) , (∃ →) のおのおのについて, その eigenvariable は side formula の先祖以外には現れないように, あらかじめ自由変数の改名をしておく.

2 GL_{ω} において許容されることについては [KN96] Proposition 3.3.

(1) P の endsequent に現れる自由変数全体を a_{1} , …, a_{k} とする. ただし endsequent に自由変数がない場合は k = 1 として, P の中で eigenvariable として使われてない任意の自由変数 a_{1} をとる.

(2) P の中の自由変数で, endsequent に現れず, eigenvariable としても使われていないもののすべてに, a_{1} を代入する. この操作によって endsequent は変わらない.

(3) 各 formula A に対して A^{∘} をつぎのとおり帰納的に定める. A が atomic ならば A^{∘} は A である. (A ⊃ B)^{∘} は A^{∘} ⊃ B^{∘} である. ¬, ∧, ∨, K_{i} , C についても同様. (∀x F (x))^{∘} は F^{∘}(a_{1}) ∧ … ∧ F^{∘}(a_{k}) である. (∃x F (x))^{∘} は F^{∘}(a_{1}) ∨ … ∨ F^{∘}(a_{k}) である. ∀ と ∃ とを含まない式はこの変換によって変わらない.

(4) P の中のおのおのの式 A を A^{∘} に書き替える. この操作によって (B) は

K_{i}F (a_{1}) ∧ … ∧ K_{i}F (a_{k}) ⟶ K_{i}(F (a_{1}) ∧ … ∧ F (a_{k}))

の形に変わるが, これは CK で ∀ も ∃ ももちいずに証明できる.

∀ と ∃ とに関する推論の変換されたものについては, 下から順につぎのように処理する.

推論 (→ ∀) は

{Γ ⟶ Θ, F (a) \atop Γ ⟶ Θ, F (a_{1}) ∧ … ∧ F (a_{k})}

の形に変わるが, 自由変数 a は lower sequent に現れないから, upper sequent に至る部分において a に a_{1} , …, a_{k} をそれぞれ代入し

\begin{matrix}Γ ⟶ Θ, F (a_{1}) & ⋯ & Γ ⟶ Θ, F (a_{k}) \\ Γ ⟶ Θ, F (a_{1}) ∧ … ∧ F (a_{k}) \end{matrix} (→ ∧)^{∗}

の形になおす. ただし, (→ ∧)^{∗} は (→ ∧) の何回かの繰り返しを意味する. (∃) についてはこれと双対.

推論 (∀ →) は

{F (t), Γ ⟶ Θ \atop F (a_{1}) ∧ … ∧ F (a_{k}), Γ ⟶ Θ}

の形に変わる. 下から順に処理しているのでこれより下には未処理の (→ ∀) , (∃ →) はなく, したがって t は eigenvariable ではないから, a_{1} , …, a_{k} のいずれかである. そのことに基いて

{F (a_{j}), Γ ⟶ Θ \atop F (a_{1}) ∧ … ∧ F (a_{k}), Γ ⟶ Θ} (∧ →)^{∗}

になおす. (→ ∃) についてはこれと双対.

他の推論についてはそれぞれ同種の推論に変換されるので問題ない. 以上の操作によって ∀ も ∃ も含まない CK の証明図が得られる. 定理 8. [Fixed point] ⊢CK CA ≡ A ∧ CK_{1}A ∧ … ∧ CK_{n}A. 証明. まず各 e に対して CA ⟶ K_{e}K_{1}A を示す. e ∗ 1 ≠ e の場合は K_{e}K_{1} = K_{e∗1} であるから

{K_{e}K_{1}A ⟶ K_{e}K_{1}A \atop CA ⟶ K_{e}K_{1}A} (C →) .

また e ∗ 1 = e の場合は e = e′ ∗ 1 となる e′ があって K_{e′}K_{1} = K_{e} ゆえに

\begin{matrix}{K_{1}A ⟶ K_{1}A \atop K_{1}A ⟶ K_{1}K_{1}A} & (K → K) \\ K_{e′}K_{1}A ⟶ K_{e′}K_{1}K_{1}A \end{matrix} ; (K → K)^{∗} ; CA ⟶ K_{e′}K_{1}K_{1}A ; (C →) .

以上で CA ⟶ K_{e}K_{1}A が示された. i = 2 , …, n に対しても同様に CA ⟶ K_{e}K_{i}A. また CA ⟶ A はあきらか. 以上のことから ⊢CK CA ⟶ A ∧ CK_{1}A ∧ … ∧ CK_{n}A.

逆に ⊢CK A, CK_{1}A, …, CK_{n}A ⟶ CA を示す. |e| = 0 の場合はあきらかに A, CK_{1}A, …, CK_{n}A ⟶ K_{e}A である. |e| > 0 の場合は e = e′ ∗ i, e ≠ e′ と表せて K_{e} = K_{e′}K_{i} ,

\begin{matrix}{K_{e′}K_{i}A ⟶ K_{e′}K_{i}A \atop CK_{i}A ⟶ K_{e′}K_{i}A} & (C →) \\ A, CK_{1}A, …, CK_{n}A ⟶ K_{e′}K_{i}A \end{matrix}(ti)^{∗} ,

ただし (ti)^{∗} は (t →) , (→ t) , (i →) , (→ i) の有限回の繰り返しを意味する.^{3}

ゆえに A, CK_{1}A, …, CK_{n}A ⟶ CA. 定理 9. [Fixed point] ⊢CK CA ≡ A ∧ K_{1}CA ∧ … ∧ K_{n}CA. 証明. 各 i について CA ⟶ K_{i}CA であり, またあきらかに CA ⟶ A であるから

CA ⟶ A ∧ CK_{1}A ∧ … ∧ CK_{n}A.

逆はつぎのとおり. |e| = 0 のとき A ⟶ K_{e}A. |e| > 0 のときは e = i ∗ e′ , e ≠ e′ と表せて K_{e} = K_{i}K_{e′} .

\begin{matrix}{K_{e′}A ⟶ K_{e′}A \atop CA ⟶ K_{e′}A} & (C →) \\ K_{i}CA ⟶ K_{e}A \end{matrix} ; (K → K) ; A, K_{1}CA, …, K_{n}CA ⟶ K_{e}A (ti)^{∗} ,

ゆえに A, K_{1}CA, …, K_{n}CA ⟶ CA. 問題 2. CK において公理 CKC の不可欠であることの証明.

GL_{ω} との関係

定理 10. CK で証明可能な sequent は GL_{ω} で証明可能である. 問題 3. Infinitary disjunction を含まず C( · ) の形以外に infinitary conjunction を含まない式 ([K99] の “cc-formula”) は, GL_{ω} で証明可能ならば CK で証明可能か? 注. 命題論理に限定すれば, GL_{ω} のある部分系に関しては成立する [K99].

Halpern and Moses の体系との関係

Halpern and Moses の体系は多様相命題論理 S4 に, C を不動点として定める公理と推論規則とをつけ加えたものである. この体系を少し修正して多様相述語論理 KD4 上の体系を作る.

まず多様相述語論理 KD4 の Hilbert style の体系は, 古典述語論理の Hilbert style の体系につぎの公理と推論規則とを各 i ∈ N についてつけ加えて得られる.

[K] K_{i}(A ⊃ B) ⊃ K_{i}A ⊃ K_{i}B .

[D] ¬K_{i}(A ∧ ¬A) .

3ここでは実は (t →) と (i →) との繰り返しである.

[4] K_{i}A ⊃ K_{i}K_{i}A.

[Barcan] ∀x K_{i}F (x) ⊃ K_{i}∀x F (x) . [Necessitation] {A \atop K_{i}A} . なお, Axiom D を Axiom T: K_{i}A ⊃ A に変更すれば S4 の体系になる. この多様相述語論理 KD4 の Hilbert style の体系に, さらにつぎの公理と推論規則とをつけ加

える. Axiom. CA ⊃ A. Axiom. CA ⊃ K_{i}A ( i ∈ N ). Axiom. CA ⊃ K_{i}CA ( i ∈ N ). Inference rule.

\begin{aligned}B ⊃ A & B ⊃ K_{1}B & … & B ⊃ K_{n}B & B ⊃ K_{1}A & … & B ⊃ K_{n}A \\ & & & B ⊃ CA \end{aligned}

この体系を仮に HM とよぶ. 定理 11. ⊢HM A ならば ⊢CK A. 証明. HM の各公理が CK で証明可能であることは容易にわかる.

\begin{matrix}B ⟶ K_{1}B & {B ⟶ K_{2}A \atop K_{1}B ⟶ K_{1}K_{2}A} (K → K) \\ B ⟶ K_{1}K_{2}A \end{matrix} ; (cut) ,

など, 以下同様にして B ⟶ K_{i}B ( i ∈ N ), B ⟶ K_{i}A ( i ∈ N ) から B ⟶ K_{e}A ( e ∈ N^{⟨ω⟩} ) が導かれるから, B ⟶ CA が得られる. 問題 4. ⊢CK A ならば ⊢HM A か? 注. 命題論理の式 A に関しては定理 7 により ⊢CK A ならば ⊢HM A であることが [K99] の結果から推測される. しかし述語論理に関しては, 共有知識述語論理の体系は recursively enumerable でないという Wolter の未発表の定理から, 否定的であると予想される.

文献

[KN96] Kaneko, Mamoru and Nagashima, Takashi: Game logic and its applications I. Studia Logica, Vol.57 (1996), pp.325–354.

[KN97a] Kaneko, Mamoru and Nagashima, Takashi: Game logic and its applications II. Studia Logica, Vol.58 (1997), pp.273–303.

[K99] Kaneko, Mamoru: Common knowledge logic and game logic. J. Symbolic Logic, 64, No. 2 (1999), pp.685–700.

[KN97b] Kaneko, Mamoru and Nagashima, Takashi: Axiomatic indefinability of common knowledge in finitary logics. In Epistemic logic and the theory of games and decisions (M. Bacharach, L. A. Gerard-Varet, P. Mongin, H. Shin eds.), Center for operations research and econometrics (CORE), 1997. pp.69–93.