Как сколемизировать множественные комбинации универсальных и экзистенциальных кванторов?

Question

Что такое сколемизированная форма (∀u∃va (u, v)) ∧ (∀x∃ya (x, y))?

Я не уверен, потому что существуют разные нормальные формы perenexвозможно:

• ∀u∃v ∀x∃y (a (u, v) ∧ a (x, y))
• ∀u∀x ∃v∃y (a(u, v) ∧a (x, y))
• …

Следуют различные сколемизированные формы:

• ∀u ∀x (a (u, f (u)) ∧ a (x, g (u, x)))
• ∀u∀x (a (u, f (u, x)) ∧ a (x, g(и, х)))

На мой взгляд, они не эквивалентны друг другу.Или я здесь не прав?

Answer 1

Да, пренекс нормальные формы не являются уникальными для данной формулы FO, и, соответственно, сколемизации не уникальны. Более простой пример для То же самое «побег из области видимости», я думаю, вы пытаетесь показать это формула ∃xAx → ∃yBy, с предшествующими формами ∀x∃y (Ax → By) и ∃y∀x (Ax → By), и соответственно сколемизации ∀x (¬ Ax ∨ Bf (x)) и ∀x (¬ Ax ∨ B a), с постоянной.

Теперь уместный вопрос: является ли неэквивалентность этих формулы имеют значение для вашей конкретной проблемы. Если это так, возможно Сколемизация - не лучший инструмент для вас: Сколемизация - это процесс предназначен для сохранения выполнимости формул, иногда за счет эквивалентности.

(и в любом случае, это хорошее упражнение, чтобы понять, почему разные сколемизации одной формулы равнозначны, если только в приведенных выше примерах)