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

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

$\mathrm{\forall }{x}_1\mathrm{\forall }{x}_2\dots \mathrm{\forall }{x}_{n}A(x_1,x_2,\dots ,x_n)$

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

Сколемізація

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

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

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

Крок 1. Привести формулу логіки першого порядку до виду:

$Q_1{x}_1{Q}_2{x}_2\dots Q_n{x}_{n}A(x_1,x_2,\dots ,x_n)$

де $Q_i$ якийсь із кванторів, а формула $A$ не містить кванторів і знаходиться в кон'юнктивній нормальній формі. Будь-яка формула логіки першого порядку еквівалентна формулі такого виду.

Крок 2. Якщо всі квантори $Q_i$ є кванторами загальності дана формула записана у формі Сколема.

Крок 3. Нехай формула має вид:

$\mathrm{\forall }{x}_1\dots \mathrm{\forall }{x}_{i-1}\mathrm{\exists }{x}_i{Q}_{i+1}{x}_{i+1}\dots Q_n{x}_{i+1}A(x_1,x_2,\dots ,x_n)$

Тоді внаслідок сколемізації одержується нова формула:

$\mathrm{\forall }{x}_1\dots \mathrm{\forall }{x}_{i-1}{Q}_{i+1}{x}_{i+1}\dots Q_n{x}_{n}A(x_1,\dots x_{i-1},f(x_1,\dots ,x_{i-1}),x_{i+1}\dots ,x_n)$

У випадку якщо квантор існування знаходиться на початку формули відбувається заміна на функцію арності 0, тобто константу.

Після цього повертаємося на крок 2.

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

Приклади

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

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

$F^{\prime }:=\mathrm{\exists }y\mathrm{\forall }w\mathrm{\exists }z(P(a,y,w)\wedge Q(z,a))$

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

$F^{″}:=\mathrm{\forall }w\mathrm{\exists }z(P(a,b,w)\wedge Q(z,a))$

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

$F^{‴}:=\mathrm{\forall }w(P(a,b,w)\wedge Q(f\left(w\right),a))$

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

Див. також

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

Посилання

• Сколемізація Шаблон:Webarchive на сайті PlanetMath.org

Джерела

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