日々の流転

λ. 「トランプの和と積のパズル」と様相論理

どう書く？.org に「トランプの和と積のパズル」という問題があった。

プログラムを書いて答えを求めることは難しくないのだけど、この手の問題を見るたびに様相論理で一般的に扱えないのかなと思ってしまう。 思っただけでちゃんと考えたことがなかったので、少し考えてみようと思う。

知識論理

こういうのを扱う様相論理として知識論理(Epistemic logic)がある。 知識論理は様相論理の一種で、□φを「φであることを知っている」と解釈する。 そして、知識論理の □ は様相論理でいうところの S5 様相になっていることが仮定される。これはつまり、以下の形の論理式が成り立つということである(ただし、◇φ := ¬□¬φ)。

K(φ,ψ) := □(φ→ψ) → □φ → □ψ

φ→ψ であることを知っていて、更に φ であることを知っているなら、ψ であることも知っている。

T(φ) := □φ → φ

φであることを知っているのなら、φである。

5(φ) := ◇φ → □◇φ

「φでないことを知らない」のなら、そのことを知っている。

さらに、ここから以下のようなことも言える。

D(φ) := □φ→◇φ

φであることを知っているなら、φでないことは知らない。

B(φ) := φ→□◇φ

φならば、「φでないことを知らない」ということを知っている。

4(φ) := □φ→□□φ

φであることを知っているなら、そのことを知っている。

背景知識

Num := {1..13} として、原子論理式の集合 { N({m,n}), S(m+n), P(m×n) | m,n∈Num } が与えられているとする。それぞれの意図している意味は次の通りである。

N({m,n})

二枚のカードの数字がm,nである。

S(n)

二枚のカードの数字の和がnである。

P(n)

二枚のカードの数字の積がnである。

以下のような論理式の集合Φが成り立つことを仮定する。

• ∨{ N({m,n}) | m,n∈Num }
• { N({m,n})→¬N({m',n'}) | m,m',n,n'∈Num, {m,n}≠{m',n'} }
• { N({m,n}) → S(m+n) | m,n∈Num }
• { N({m,n}) → P(m×n) | m,n∈Num }
• { S(n)→¬S(m) | m,n∈Num, m≠n }
• { P(n)→¬P(m) | m,n∈Num, m≠n }

問題の記述

これでようやく問題が記述できる。

ここでは複数の人が登場するので「φであることをXさんが知っている」ということを [X]φ で表す(各 [X] はそれぞれS5様相だとする)。 そうすると、Xさんが数字を分かることは α(X) := ∨{ [X]N({m,n}) | m,n∈Num } で表すことが出来る。

• Aさんは積を知っているので ∨{ [A]P(m×n) | m,n∈Num }
• 同様に、Bさんは和を知っているので ∨{ [B]S(m+n) | m,n∈Num }
• Aさんは(この情報だけでは)数字が分からないので ¬α(A)
• Bさんも(この情報だけでは)数字が分からないので ¬α(B)
• BさんはAさんが「分かりません」というのは分かっていたので [B]¬α(A)

これを聞いたあとのAさんが知っているということは、元のAさんが知っているということとは別なので、[A1] という様相で扱うことにする。

• Aさんが元々知っていた事はすべて知っているので、[A]φ → [A1]φ
• 今聞いた情報を知っているので [A1](¬α(B) ∧ [B]¬α(A))
• それを聞いて答えがわかっているので α(A1)

同様に、これを聞いたあとのBさんが知っているということを [B1] という様相で扱うことにする。

• Bさんが元々知っていた事はすべて知っているので [B]φ → [B1]φ
• 「Aさんに話した内容をAさんが知っている」ことを知っているので、[B1][A1](¬α(B) ∧ [B]¬α(A))
• 今聞いた情報を知っているので [B1]α(A1)
• それを聞いて答えがわかっているので α(B1)

どうやって解くか

こうやって論理式で記述できたら、後は定理証明器やモデル検査で答えが求まらないものだろうか。 それはまた今度考える。