Нормальна форма формули у логіці предикатів

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до навігації Перейти до пошуку

Нормальна форма формули у логіці предикатів — це формула, яка містить лише операції кон'юнкції, диз'юнкції та кванторні операції, а операція заперечення відноситься до елементарних формул.

З допомогою рівностей алгебри висловлень й логіки предикатів кожну формулу логіки предикатів можна привести до нормальної формули.[1]

Теорема про нормальну форму

[ред. | ред. код]

Теорема: Кожна формула логіки предикатів має нормальну форму.

Доведення: Перш ніж доводити теорему, встановимо 4 равносильності, які необхідні нам надалі. В них передбачається, що формула Н не містить вільної змінної х:

Встановимо першу з цих рівносильностей. Решта - аналогічно.


Нехай істинна для деякої області М. Тоді на М істинно чи , чи . В першому випадку тотожно істинний на М предикат і через те, що не містить х, теж тотожно істинний на М предикат, і тоді - істинно. У другому випадку, якщо істинно , то істинно і незалежно від х, а значить з М.

Нехай тепер хибно. Тоді і хибні. Тобто існує , такий що хибно. Але тоді хибно, бо хибно.


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



Тоді формулі рівносильна формула , яка може завжди бути приведена до нормальної форми з використанням рівностей 1 – 2:



Таким чином, отримана нормальна форма формули . Аналогічно, з рівностей 3,4 отримаємо, що можна побудувати нормальну форму і для . Нарешті, якщо відома нормальна форма формули , то нормальна форма має вигляд:



Таким чином встановлено, що будь-яка формула логіки предикатів має нормальну форму.

Алгоритм приведення формули до нормальної форми

[ред. | ред. код]

Для приведення формули до нормальної форми потрібно виконати наступні операції:

  1. виключити операції , ~, якщо вони є;
  2. зменшити область знаків заперечення;
  3. перейменувати змінні так, щоб можна було винести квантори в початок формули.


Приклад

[ред. | ред. код]


Примітки

[ред. | ред. код]
  1. Математическая логика. Предваренная нормальная форма (рус.). Архів оригіналу за 29 листопада 2014. Процитовано 20 листопада 2014.


Посилання

[ред. | ред. код]