日々の流転

λ. 推移閉包は一階述語論理では表現できないのね

先日の「SPASSで知識の論理を使って論理パズルを解く?」についてちと考えていて、共通認識を扱う知識論理を一階述語論理に翻訳するには推移閉包(transitive closure)を表現する必要があることに気付いた。 それ自体はここではどうでも良いのだけど、どうにも推移閉包をうまく表現できなくて困った。

例えば、TがRの推移閉包であることを表すには「∀x,y. (T(x,y) ⇔ (R(x,y) ∨ (∃z. R(x,z)∧T(z,y))))」のような公理では不十分で、これだと最小不動点以外の解を排除できないため、「有限回のRで到達可能」ということをちゃんと表せていない。うーむ。

検索してみると、一階述語論理で推移閉包を表現できないというのは随分有名な話だったようだ。知らなかった……orz　しかし、こないだの「整礎性は一階述語論理では表現できないのね」といい、一階述語論理の表現力って僕が漠然と思っていたよりも、ずいぶんと限定されたものなのだな。