閉世界仮説と完全性

Prologの意味論で、閉世界仮説とかいうのがあったけど、アリャいったい何だったんだろう。いまだにわからん、つうか、一度も考えた事ないからわからんで当たり前だが。

「Aの証明が失敗する」と「Aが証明できない」と「¬Aが真]を同一視するような話だったと思う。この３つはまったく別物だよね、ふつうに考えれば。

• Aの証明が失敗したのは、たまたまかもしれない。他の戦略では成功するかも。
• 「Aが証明できない」は構文論的な（メタな）言明。Aが証明できないことが、「¬Aが証明できる」を保証しない。
• 「¬A が真」は意味論的な主張。

演繹系とモデルがあって、完全なら、

• Aが真 ⇒ Aが証明できる

となるから、対偶をとって二値論理として計算すると

• Aが証明できない ⇒ （Aが真でない ≡ Aが偽 ≡ ¬Aが真）

となる。ってことは、閉世界ってのは、完全性が成立しているってこと？ さらに、

• ある方法でAの証明が失敗する ⇒ Aは証明できない

であるためには、証明のアルゴリズムに停止性とか決定性とかが要求されそうだ。

閉世界ってのは、アルゴリズムで何でも決定できるような、メチャクチャ都合がいい世界ってことか？ Prologの意味論の本が一冊あったような気もする。探してみるか？ いや、めんどい。