孤立したEXISTS句のskolemisationはどのように機能しますか？

Question

私が持っている場合と同様に式：EはFAの外にある場合

1. と交換してください：（=が存在するFA =すべての場合/ E）

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

   skolemisationの

   のルールがあると言います定数または

2. EがFAの内側にある場合FAの外側のすべての変数を引数として含む新しい関数で置換されます。

この場合、私は何をしますか？ Exists数量子を削除することはできますか？またはそれを定数で置き換えることはできますか？

ありがとうございます！だから私は、外部からのすべてのVARSを含む関数で∃z置き換えられました

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

：あなたの二skolemisationルールを適用し、

今

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

：

Answer 1

まず、この使用して標準的な表記法を記述します。

今のところ、これはまだのconjuctive prenexノーマル形式ではないため、Skolemのノーマル形式ではありません。数式では依然として多くの論理和（∨）が使用されています。それらを削除することはあなた次第です。