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

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

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

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

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

${\displaystyle Q_{1}x_{1}Q_{2}x_{2}\ldots Q_{n}x_{n}A(x_{1},x_{2},\ldots ,x_{n})}$

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

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

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

${\displaystyle \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})}$

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

${\displaystyle \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, даний алгоритм зрештою дає формулу у формі Сколема.

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

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

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

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

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

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

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

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

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

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

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