Как работает скиммизация одиночных условий EXISTS?

Question

Если у меня есть формула, как:

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

(FA = для всех/Е = Exists)

Правила skolemisation говорят, что:

1. если Е находится за пределами FA заменить константа или
2. , если E внутри FA заменить новой функцией, содержат все вары извне FA в качестве аргументов.

Так что мне делать в этом случае? Могу ли я просто удалить квантор Exists или заменить его константой?

Спасибо!

Answer 1

Сначала пишет это, используя стандартные обозначения:

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

Теперь, применяя свое второе правило skolemisation:

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

Так я заменил ∃z с функцией, содержащей весь ВАР извне.

Теперь это еще не в Сколеме нормальная форма, потому что это не в Соединительный prenex нормальная форма: формулы все еще используют множество дизъюнкций (∨). Удаление этих данных остается за вами.