閉世界仮説

閉世界仮説（へいせかいかせつ、）は、現時点で真であると判明していないことは偽であると仮定することを意味する。論理学では、Raymond Reither が閉世界仮説を形式化した。閉世界仮説の逆を開世界仮説（Open world assumption）と呼び、知識の欠如を偽とは見なさない。
概要.
失敗による否定（Nagation as failure）は閉世界仮説と関連しており、真であると証明されなかった述語は偽であると見なされる。
ナレッジマネジメントでは、閉世界仮説が少なくとも2つの状況で使われる。第一に、知識ベースが完成した時点で、そこに含まれない知識は偽であるとされる。例えば、企業の従業員のデータベースが完全であれば、そこに記録されていない人は従業員ではない。第二に、知識ベースが不完全であるときでも、そこにない知識は偽であるとして回答することが最善の場合である。例えば、以下のような編集者と記事名の表がデータベースにあったとき、"Formal Logic" の編集に関わっていない編集者というクエリに対しては “Sarah Johnson” と答えることが期待される。
閉世界仮説では、この表が完全である（全ての編集者と記事の対応が格納されている）と仮定され、この表の中では Sarah Johnson だけが Formal Logic に関わっていない編集者とされている。もしここで開世界仮説を採用すれば、この表には全ての情報（編集者と記事の対応）が格納されているとは限らないと考えられ、答えが得られない。つまり、この表に載っていない編集者がどれだけいるか、Sarah Johnson が関わってこの表に載っていない記事がどれだけあるか分からないのである。
論理学における形式化.
論理学における閉世界仮説の最初の形式化は、知識ベースに含まれないリテラル群について、その否定を知識ベースに加えることとされた。この場合、知識ベースがホーン節で表されるなら一貫性が保たれるが、そうでない場合は必ずしも一貫性は保たれない。例えば、次のような知識ベース
では、formula_2 も formula_3 も含まれていない（フレッドはイギリス人かアイルランド人であり、どちらであるかは知識として確定していない）。
ここで、それらの否定を知識ベースに加えると次のようになる。
これでは一貫性がない（フレッドはイギリス人でもアイルランド人でもないことになり、元の知識と矛盾する）。換言すれば、閉世界仮説を形式化すると一貫性のある知識ベースが一貫性を失う場合がある。閉世界仮説を導入して一貫性が失われないのは、知識ベース formula_5 の全てのエルブランモデルの交差と formula_5 のモデルとが等価である場合だけである。命題論理の場合、この条件は formula_5 が単一の最小のモデルしか持たないことと等価であり、モデルが最小とは真である変項の部分集合を持つ他のモデルが存在しないことを意味する。
このような問題を起こさない別の形式化が提案されてきた。以下では、知識ベース formula_5 は命題論理的であると仮定する。どのような場合も、閉世界仮説の形式化では formula_5 において否定してもよい論理式の否定形を formula_5 に追加することを基本とする。つまり、それらの論理式は偽であると仮定される。換言すれば、命題論理式 formula_5 に閉世界仮説を適用すると次のような論理式が生成される。
集合 formula_13 は formula_5 において否定してもよい論理式の集合である。この formula_13 の定義を変えることで閉世界仮説の形式化が変わってくる。以下に formula_16 の様々な定義によって得られる（閉世界仮説の）形式化を列挙する。
ECWA とサーカムスクリプションの形式化は命題論理においては等価である。ある論理式が閉世界仮説の下で別の論理式に含まれているかどうかを確かめることの複雑性は、通常は論理式の多項式階層の第二レベルであり、ホーン節についてはPとcoNPの間にある。本来の閉世界仮説を導入することで一貫性を失うかどうかの判定はNP預言機械を最大でも対数回呼び出す必要があるが、この問題の正確な複雑性は未知である。