日々の流転

λ. 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」と書くと、稠密性と双対の関係にあることが分かる。 考えてみれば当たり前だけど、最近まで気付いていなかった。