包摂(subsumption)

質問

やや筋違いかもしれませんが，プログラミング，論理学，数学（？）の境目のような疑問です．

一階述語論理の演算に包摂(subsumption)という演算がありますが，この定義が今ひとつわかりません．ある本によると「論理式Aが論理式Bを包摂するとは，ある代入θがあってAθ⊆Bとなることだ」と書いてありました．しかし2つの論理式の包含関係というのは，どういう意味なのでしょうか？つまりAθもBも論理式であるわけですが，その間に⊆という演算が成立するということは，どいういう意味なのでしょう？A，Bをtrueにするインスタンスの集合という観点からの包含関係なのでしょうか？

回答No.1

stomachman

そもそも「包摂」は一階述語論理の演算ではありませんで、この用語は典型的には「導出原理」の理論に出て来ます。「導出原理」は一階述語論理で書かれた命題を機械的(つまり自動的)に証明（または反駁）する方法です。その際、「論理式Aが論理式Bを包摂する」のではなくて、「節Aが節Bを包摂する」。そして「節」とは「リテラル（すなわち原子式もしくは原子式の否定）」という記号列を要素とする有限集合であって、これは一連の機械的操作において論理式（という記号列）をパーツにバラして扱うための手段です。

　という訳で、証明の対象となる一階述語論理と、証明の方法の理論と（さらには論理式の意味論（モデル(解釈)の理論）も？）を混同なさっているようにお見受けします。「一階述語論理」という形式言語をじっくり復習した上で、「導出原理」等の自動証明アルゴリズムの勉強に取りかかる方が宜しいかと思います。