Нормальна форма Сколема

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

У логіці першого порядку деяка логічна формула є записаною в нормальній формі Сколема , якщо вона має вигляд:

\forall x_1 \forall x_2 \ldots \forall x_n A(x_1,x_2,\ldots,x_n)

де формула A(x_1,x_2,\ldots,x_n) записана в кон'юнктивній нормальній формі, тобто є кон'юнкцією диз'юнкцій атомарних формул чи їх заперечень. Будь-яка формула логіки першого порядку може бути зведена до формули у нормальній формі Сколема за допомогою процесу, що отримав назву сколемізація. Одержана внаслідок сколемізації формула не є логічно еквівалентна вихідній формулі, проте вона є виконуваною в тому і тільки тому випадку коли такою є вихідна формула (тобто для деякої формули існує модель в тому і тільки тому випадку, коли вона існує для формули одержаної внаслідок процесу сколемізації) .

Сколемізація[ред.ред. код]

Сколемізація полягає у заміні змінних, що квантифікуються квантором існування на терми виду f(x_1,\ldots,x_n), де f — новий функційний символ, що не зустрічається в інших місцях формули. Змінні x_1,\ldots,x_n , від яких залежить дана функція, це змінні, що квантифікуються кванторами загальності і квантори яких знаходяться перед квантором змінної, що замінюється на f(x_1,\ldots,x_n).

Наприклад, формула \forall x \exists y \forall z. P(x,y,z) не знаходиться в нормальній формі Сколема, тому що містить квантор існування \exists y. Процес сколемізації замінює y на f(x), де f є новим символом функції, і видаляє знак квантора існування. Результуюча формула має вигляд \forall x \forall z . P(x,f(x),z). Терм Сколема f(x) містить x але не z оскільки квантор, який є видаленим \exists y знаходиться в області дії \forall x і не знаходиться в області дії \forall z.

Дану процедуру можна записати більш формально:

Крок 1. Привести формулу логіки першого порядку до виду:
Q_1 x_1 Q_2 x_2 \ldots Q_n x_n A(x_1,x_2,\ldots,x_n)
де Q_i якийсь із кванторів, а формула A не містить кванторів і знаходиться в кон'юнктивній нормальній формі. Будь-яка формула логіки першого порядку еквівалентна формулі такого виду.
Крок 2. Якщо всі квантори Q_i є кванторами загальності дана формула записана у формі Сколема.
Крок 3. Нехай формула має вид:
\forall x_1 \ldots \forall x_{i-1} \exists x_i Q_{i+1} x_{i+1} \ldots  Q_{n} x_{i+1}A(x_1,x_2,\ldots,x_n)
Тоді внаслідок сколемізації одержується нова формула:
\forall x_1 \ldots \forall x_{i-1}  Q_{i+1} x_{i+1} \ldots  Q_{n} x_{n}A(x_1,\ldots x_{i-1},f(x_1,\ldots,x_{i-1}),x_{i+1} \ldots,x_n)
У випадку якщо квантор існування знаходиться на початку формули відбувається заміна на функцію арності 0, тобто константу.
Після цього повертаємося на крок 2.

Оскільки при кожному виконанні кроку 3 кількість кванторів існування зменшується на 1, даний алгоритм зрештою дає формулу у формі Сколема.

Приклади[ред.ред. код]

F:=\exists x\exists y\forall w\exists z\left(P\left(x,y,w\right)\land Q\left(z,x\right)\right) Дана функція не є в нормальній формі Сколема, проте знаходиться у формі одержуваній після першого кроку алгоритму.

  • Застосовуємо сколемізацію до \exists{x} замінюючи x константою a :

F':=\exists y\forall w\exists z\left(P\left(a,y,w\right)\land Q\left(z,a\right)\right)

  • Застосовуємо сколемізацію до \exists{y} замінюючи y константою b

F'':=\forall w\exists z\left(P\left(a,b,w\right)\land Q\left(z,a\right)\right)

  • Застосовуємо сколемізацію до \exists{z}. Оскільки перед даним квантором знаходиться \forall w то здійснюємо заміну на унарну функцію від змінної w:

F''':=\forall w\left(P\left(a, b, w\right)\land Q\left(f\left(w\right), a\right)\right)

Остання формула знаходиться в нормальній формі Сколема.

Див. також[ред.ред. код]

Посилання[ред.ред. код]

Джерела[ред.ред. код]

Shawn Hedman. A First Course in Logic. Oxford University Press 2004 ISBN 0198529805