トップ «前の日記(2007-08-01) 最新 次の日記(2007-08-03)» 月表示 編集

日々の流転


2007-08-02 [長年日記]

λ. Modal Algebras

昔、途中で挫折した First Steps in Modal Logic を再び読んでいるのだが、命題 3.4 の自然言語で書かれた証明に頭がこんがらがってきた。以前に読んだ時にはあっさり理解できたはずなのだが……。

これはどういう命題かというと、遷移関係が

  1. 反射的(reflexive)
  2. 推移的(transitive)
  3. pathetic: a R b ⇒ a=b
  4. 稠密(dense): a R b ⇒ ∃x. a R x R b

であることと、□X = {a | ∀x. a R x ⇒ x∈X} で定義される演算子 □ が

  1. Deflationary: □X⊆X
  2. Nearly inflationary: □X⊆□□X
  3. Inflationary: X⊆□X
  4. Nearly deflationary: □□X⊆□X

であることが、それぞれ同値だという命題。

それで、「頭がこんがらがるのは自然言語で証明が書かれているからだ」と思い、Agdaで書いてみた(ModalAlgebras.agda) 一応、頭はスッキリしたが、かえってややこしくなっている気もしないでもない。

追記

ちなみに、反射律を「a=b ⇒ aRb」と書くと、patheticであることと双対の関係にあることが分かる。 同様に、推移律を「(∃x. a R x R b) ⇒ a R b」と書くと、稠密性と双対の関係にあることが分かる。 考えてみれば当たり前だけど、最近まで気付いていなかった。