У логіці першого порядку деяка логічна формула є записаною в нормальній формі Сколема , якщо вона має вигляд:
де формула записана в кон'юнктивній нормальній формі, тобто є кон'юнкцією диз'юнкцій атомарних формул чи їх заперечень. Будь-яка формула логіки першого порядку може бути зведена до формули у нормальній формі Сколема за допомогою процесу, що отримав назву сколемізація. Одержана внаслідок сколемізації формула не є логічно еквівалентна вихідній формулі, проте вона є виконуваною в тому і тільки тому випадку коли такою є вихідна формула (тобто для деякої формули існує модель в тому і тільки тому випадку, коли вона існує для формули одержаної внаслідок процесу сколемізації) .
Сколемізація
Сколемізація полягає у заміні змінних, що квантифікуються квантором існування на терми виду , де — новий функційний символ, що не зустрічається в інших місцях формули. Змінні , від яких залежить дана функція, це змінні, що квантифікуються кванторами загальності і квантори яких знаходяться перед квантором змінної, що замінюється на .
Наприклад, формула не знаходиться в нормальній формі Сколема, тому що містить квантор існування . Процес сколемізації замінює на , де є новим символом функції, і видаляє знак квантора існування. Результуюча формула має вигляд . Терм Сколема містить але не оскільки квантор, який є видаленим знаходиться в області дії і не знаходиться в області дії .
Дану процедуру можна записати більш формально: Крок 1. Привести формулу логіки першого порядку до виду:
де якийсь із кванторів, а формула не містить кванторів і знаходиться в кон'юнктивній нормальній формі. Будь-яка формула логіки першого порядку еквівалентна формулі такого виду. Крок 2. Якщо всі квантори є кванторами загальності дана формула записана у формі Сколема. Крок 3. Нехай формула має вид:
Тоді внаслідок сколемізації одержується нова формула:
У випадку якщо квантор існування знаходиться на початку формули відбувається заміна на функцію арності 0, тобто константу. Після цього повертаємося на крок 2.
Оскільки при кожному виконанні кроку 3 кількість кванторів існування зменшується на 1, даний алгоритм зрештою дає формулу у формі Сколема.
Приклади
Дана функція не є в нормальній формі Сколема, проте знаходиться у формі одержуваній після першого кроку алгоритму.
Застосовуємо сколемізацію до замінюючи константою :
Застосовуємо сколемізацію до замінюючи константою
Застосовуємо сколемізацію до . Оскільки перед даним квантором знаходиться то здійснюємо заміну на унарну функцію від змінної :
Остання формула знаходиться в нормальній формі Сколема.
Див. також Логіка першого порядку Нормальна форма формули у логіці предикатів Кон'юнктивна нормальна форма Диз'юнктивна нормальна форма Квантор
Посилання Сколемізація на сайті PlanetMath.org
Джерела Shawn Hedman. A First Course in Logic. Oxford University Press 2004 ISBN 0198529805