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

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

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

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

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

Наприклад, формула не знаходиться в нормальній формі Сколема, тому що містить квантор існування . Процес сколемізації замінює на , де є новим символом функції, і видаляє знак квантора існування. Результуюча формула має вигляд . Терм Сколема містить але не оскільки квантор, який є видаленим знаходиться в області дії і не знаходиться в області дії .

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

Крок 1. Привести формулу логіки першого порядку до виду:
де якийсь із кванторів, а формула не містить кванторів і знаходиться в кон'юнктивній нормальній формі. Будь-яка формула логіки першого порядку еквівалентна формулі такого виду.
Крок 2. Якщо всі квантори є кванторами загальності дана формула записана у формі Сколема.
Крок 3. Нехай формула має вид:
Тоді внаслідок сколемізації одержується нова формула:
У випадку якщо квантор існування знаходиться на початку формули відбувається заміна на функцію арності 0, тобто константу.
Після цього повертаємося на крок 2.

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

Приклади

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

  • Застосовуємо сколемізацію до замінюючи константою  :

  • Застосовуємо сколемізацію до замінюючи константою

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

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

Див. також

Посилання

Джерела

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

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.