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

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

$\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)$

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

Див. також

• Логіка першого порядку
• Нормальна форма формули у логіці предикатів
• Кон'юнктивна нормальна форма
• Диз'юнктивна нормальна форма
• Квантор

Посилання

• Сколемізація [Архівовано 27 лютого 2006 у Wayback Machine.] на сайті PlanetMath.org

Джерела

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