logic - 孤立した EXISTS 句のスコーレミゼーションはどのように機能しますか?

Question

次のような式がある場合：

FAx FAy (Ez(!A(x,z) v !A(y,z)) v B(x,y))

(FA = すべての場合 / E = 存在する)

スコーレミゼーションのルールは次のように述べています。

1. E が FA の外にある場合、定数または
2. E が FA の内部にある場合、FA の外部からのすべての変数を引数として含む新しい関数に置き換えます。

では、この場合はどうすればよいでしょうか。Exists 量指定子を単に削除することはできますか、それとも定数に置き換えることはできますか?

ありがとう！

Answer 1

最初に、標準表記法を使用してこれを書きます。

∀x∀y(∃z(!A(x,z)∨!A(y,z))∨B(x,y))

次に、2 番目の skolemisation ルールを適用します。

∀x∀y((!A(x,f(x,y))∨!A(y,f(x,y)))∨B(x,y))

そこで、∃z を外部からのすべての変数を含む関数に置き換えました。

さて、これはまだ Skolem 標準形ではありません。接続冠頭標準形ではないためです。式は依然として多くの選言 (∨) を使用しています。それらを削除するのはあなた次第です。