2005/07/06 志村先生 [知識の論理] # 次のような様相の解釈の一つを考える □A : A であることを知っている # この場合は.. □A \imp A # A であることを知っていれば A は正しい □(A\imp B) \imp ( □A \imp □B ) # は正しいと考えてよい □A \imp □□A # これは、微妙 ( 成立していたり、そうでなかったりするが.. ) A --- # 事実なら、「知っている」 □A # ここまでの性質を考えると、公理 S4 をみたしている。 # ただ、ここまでは、特定な個人に特定して議論しているが、しかし、色々な主義主張をする人間がいる。 [定義] I : 人の集合 i \in I に対し □_i A : i は、A であることを知っている。 # 人によって、知っていたり、知らなかったりする。 あるいは、 K_i A と書く ( K は knowledge の K, 「知識」を扱う場合にはこちらを使うことが多い )。 # 例えば、ゲームのプレイヤーの状況を考える時に、利用できる # プレイヤーによって、知識が異る これを用いて、ゲーム等の記述をすることを考える # ここで、次のような問題が一つある.. # ゲームのルールは、参加者「全員」が知っている必要がある 全員が知っている情報 => common knowledge ゲームのルール 自然法則 (?) # 特定なプレイヤーが特定な情報をもっていることを、他のプレイヤーが知っているという状況も考える必要がある [def] C(A) : A は common knowledge である とは、 A は正しい K_i A は正しい ( i \in I ) K_j K_i A は正しい # 他のプレイヤーに関する情報 # より一般に.. K_i_1 K_i_2 .. k_i_n A は正しい ( i_1, .., i_n \in I ) これが、全部成立すること # これは、一つ論理式で書けない # => 新しい様相 C を導入せざるを得ない # => C に関する公理を追加する [C に関する公理] C(A) \imp K_i_1 K_i_2 .. k_i_n A ( i_1, .., i_n \in I の有限列 ) # 無限個の公理になっているということに注意 C(A \imp B) \imp ( C(A) \imp C(B) ) # C(A) を証明するのは大変かも.. A ---- # 論理的に導きだすことが可能なら、common C(A) # => Player に無限の推理力を仮定している !! # まだ、足りない.. # もう一つ追加する必要があるが、それには色々流儀がある # [例] nessseary rule に相当するもの # ..., K_1K_2..A, ... # ------------------- # 全てが成立すれば C(A) # C(A) # # C(A) を省略記法だと思うならこれは自然 # # しかし、無限の処理が必要なので、好まれない [S4 によるゲームの記述例 : 赤い帽子の問題] - a, b, c の三人が、この順に縦一列に並んでいる。 - a, b, c のそれぞれは、赤または白の帽子を被っている - 縦一列に座っているので、後の人は前の人の帽子の色を見ることができる a は、b, c の帽子の色を見ることができる b は c の帽子の色を見ることができる # その他の組み合わせは、見ることができない - 少くても一人が赤い帽子を被っていると三人に「同時」に報せる # これは common knowladge であることに注意 # すると... a に帽子の色を聞くと.. 解らない b に帽子の色を聞くと.. 解らない c に帽子の色を聞くと.. 自分は「赤」だと解る # となる.. ( why ? ) ## 色々と難しい問題がある ## 個々に伝えた場合は駄目 ## 「少くても一人が赤い帽子を被っている」が common knowladge でなくなるから.. # S4 を使って、この問題を記述してみる。 r_a : a は赤い帽子を被っている w_a : a は白い帽子を被っている r_a \or w_a, \not ( r_a \and \w_a ) r_b \or w_b, \not ( r_b \and \w_b ) r_c \or w_c, \not ( r_c \and \w_c ) # 各々は、赤白どちらかの帽子を被っている # しかも、同時に被ることはない r_c \imp K_b r_c w_c \imp K_b w_c r_c \imp K_a r_c w_c \imp K_a w_c r_b \imp K_a r_b w_b \imp K_a w_b # 前の人の帽子を知ることができる r_a \or r_b \or r_c # 誰かは、赤い帽子を被っている # 他にも色々な規則が必要 # 自分自身は、白か赤の帽子を被っていると知っている # ここには、三人しかいない (a の後に人はいない..) これらの事実は、全て Common Knowladge である必要がある 特に C(r_a \or r_b \or r_c) であること (全員に同時に報せる) が重要 # K_a (r_a \or r_b \or r_c) # K_b (r_a \or r_b \or r_c) # K_c (r_a \or r_b \or r_c) # # 個々に報せる # ではいけない。 ここまでの事実を全て A で表現することにする。 『「a は自分の帽子の色が解る(K_a r_a \or K_a w_a)」が成立しない』をどう表すか ? # これは、『「A \imp ( K_a r_a \or K_a w_a )」が証明できない』ことを意味するが、これはここでは使わない # [注意] K_a ( r_a \or w_a ) は成立するが、これと、 # K_a r_a \or K_a w_a は異る a の発言 : 「自分の帽子の色が解らない」によって、 A \and C(\not (K_a r_a \or K_a w_a)) # と、「知識」が増えている。 ## C(\not (K_a r_a \or K_a w_a)) は、『「A \imp ( K_a r_a \or K_a w_a )」が証明できない』より、強いことをいっていることに注意 b の発言 : 「自分の帽子の色が解らない」によって、 A \and C(\not (K_a r_a \or K_a w_a)) \and C(\not (K_b r_a \or K_b w_a)) この結果として、 A \and C(\not (K_a r_a \or K_a w_a)) \and C(\not (K_b r_a \or K_b w_a)) \imp r_c が証明できる !! # これが証明できれば、ネセステーションルールのようなものがあるので、r_c が common knowladge になる ( つまり C(r_c) が証明できる ) # どうやって証明するか ? # まず.. A \and w_b \and w_b \imp K_a r_a が成立する。 ∵) C(w_b \imp k_a w_b) C(w_c \imp k_a w_c) なので、 A \and K_a w_b \and K_a w_c また、 C(w_b \and w_c \imp r_a) ↓ K_a(w_b \and w_c \imp r_a) ↓ ∵ K_a (A\imp B) \imp (K_a A \imp K_a B) K_a w_b \and K_a w_c \imp K_a r_a 上記の式の対偶を取ることにより A \and \not K_a r_a \imp ( \not (w_b \and w_c) ) ------------------- r_b \or r_c ところが 「a の発言」から、 A \and C(\not K_a r_a) # \not K_a r_a が発言により、Common Knowladge へ よって、 A \and C(\not K_a r_a) \imp C(r_b \or r_c) 同様に、 A \and C(\not K_a r_a) \and w_c \imp K_b r_b よって、 A \and C(\not K_a r_a) \and \not K_b r_b \imp \not w_c A \and C(\not K_a r_a) \and \not K_b r_b \imp r_c 同様に「b の発言」から、 A \and C(\not K_a r_a) \and C(\not K_b r_b) \imp r_c # 発言の中で、\not K_a w_a や \not K_b w_b が不要だった ## 以上、「意味 = モデル」の世界で、命題の真偽を議論したが、実際は、最初に述べた公理を利用することによって、正しい命題は、証明できるので、応用の場合は、その証明を実際に行うことになる。 [S4 によるゲームの記述例 : 赤い帽子の問題 #2] - n 人が輪になって中央を向いて並んでいる # つまり、自分の帽子以外は、全て見ることができる - それぞれは赤または白の帽子を被っている - 少くても一人は赤い帽子を被っている - 自分の帽子の色がわかった人は挙手をしなさい # 挙手をしたかどうかも、全員に解る これを何度繰り返すと、赤い帽子を被った人が k 人なら k 回目に同時に、挙手する。 # 状況の記述 C( r_i \or w_i ), C( \not ( r_i \and w_i ) ) # 全ての人は赤か白の帽子を被り、同時には被らない C( r_j \imp k_i r_j ), C( w_j \imp k_i w_j ) ( for i \ne j ) # 他人の帽子の色は解る C( r_1 \or .. \or r_n ) # 誰かは赤い帽子を被っている。 「1 回目に誰も挙手しない」はどう表すか ? # ここが微妙 \not ( K_i r_i \or K_i w_i ) r_1 \and w_2 \and .. \and w_n \imp K_1 r_1 なので、前の例と同様に情報量が増えて.. [注意] k>1 個の赤い帽子があれば、k-1 回目まで、手をあげないことは、推論できる => しかし、確認しないといけない