量化様相論理で有名なバーカン式についてのメモ。
その証明
時制論理で有名なアーサー・プライアーは、S5の様相命題論理に古典一階論理の公理を追加すると、バーカン式と逆バーカン式が証明できることを示した（1956年）。そして、S5より弱くできないか、と考えたE. J. レモンは、逆バーカン式はKで、バーカン式はKBで証明できることを示した。
ヒューズ＆クレスウェルの教科書に基づいて、まずは、逆バーカンの証明をみてみよう。
- ∀xα → α 全称例化
- □(∀xα → α) 必然化
- □∀xα → □α 分配
- □∀α → ∀x□α 全称般化
つぎに、少し厄介なバーカン式の証明
- ∀x□α → □α 全称例化
- □(∀x□α → □α) 必然化
- ◇∀x□α → ◇□α 分配
- ◇∀x□α → α B
- ◇∀x□α → ∀xα 全称汎化
- □(◇∀x□α → ∀xα) 必然化
- □◇∀x□α → □∀xα 分配
- ∀x□α → □∀xα B
バーカン式と逆バーカン式にはそれぞれ反例がありそうなので、この証明を退けたければ、どれかしらの前提を捨てる必要がある。一般的には、全称例化を諦めるのかな。
厳密含意との関連
一階論理の妥当式である分配法則
- ∀x(α→β)→(∀xα→∀xβ)
にあらわれる実質含意を厳密含意に置き換えると
- ∀x□(α→β)→□(∀xα→∀xβ)
となる。一見すると、これは妥当式にみえるが、証明にはバーカン式
- ∀x□φ→□∀xφ
を使う*1。証明はシンプルである。まず、φにα→βを代入して
- ∀x□(α→β)→□∀x(α→β)
を得る。分配法則∀x(α→β)→(∀xα→∀xβ)は妥当式であるから、必然化により
- □[∀x(α→β)→(∀xα→∀xβ)]
が得られる。ここから公理Kとmodus ponensにより
- □∀x(α→β)→□(∀xα→□∀xβ)]
が得られる。→の推移性により
- ∀x□(α→β)→□(∀xα→∀xβ)
となる（証明終）。
認識論理との関連
ボックスを知識として解釈すると、バーカン式は
- ∀xK(F(x))→K∀x F(x)
となる。前件は内部量化になっているので、事象様相で解釈する必要がある。これに対する反例は、すべての対象を見知っていて、それらが全部Fだと知っているが、自分が見知っている対象がすべての対象だということを知らない、といった状況だろうか。
*1:というか、これを証明するために、バーカンはバーカン式を措定したといった方がただしいかも。
