Нормальна форма формули у логіці предикатів — це формула, яка містить лише операції кон'юнкції, диз'юнкції та кванторні операції, а операція заперечення відноситься до елементарних формул.
З допомогою рівностей алгебри висловлень й логіки предикатів кожну формулу логіки предикатів можна привести до нормальної формули.[1]
Теорема:
Кожна формула логіки предикатів має нормальну форму.
Доведення:
Перш ніж доводити теорему, встановимо 4 равносильності, які необхідні нам надалі. В них передбачається, що формула Н не містить вільної змінної х:
![{\displaystyle \forall xW(x)\lor H=\forall x(W(x)\lor H)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9b0b412708bfcbc8d6668809b5e4f6fc2010f255)
![{\displaystyle \exists xW(x)\lor H=\exists x(W(x)\lor H)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/57f3446fcf2a2b6bb9842a5662e6fe3fde8b6a14)
![{\displaystyle \forall xW(x)\land H=\forall x(W(x)\land H)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e9c69a8ec7f847bff4470b257922aaa4fce0dc46)
![{\displaystyle \exists xW(x)\land H=\exists x(W(x)\land H)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ad016945136314f15d2d0f10e49069de5a55f28c)
Встановимо першу з цих рівносильностей. Решта - аналогічно.
Нехай
істинна для деякої області М. Тоді на М істинно чи
, чи
. В першому випадку
тотожно істинний на М предикат і через те, що
не містить х,
теж тотожно істинний на М предикат, і тоді
- істинно. У другому випадку, якщо істинно
, то істинно і
незалежно від х, а значить
з М.
Нехай тепер
хибно. Тоді
і
хибні. Тобто існує
, такий що
хибно. Але тоді
хибно, бо
хибно.
Доведемо тепер теорему методом індукції. Для елементарних формул наше твердження істинне, бо вони самі є нормальними формами. Будь-яку формулу можна записати, використовуючи операції
, тому достатньо показати, що якщо
і
мають нормальні форми, то і
,
,
теж мають нормальні форми. Нехай
і
мають нормальні форми
і
, де
Тоді формулі
рівносильна формула
, яка може завжди бути приведена до нормальної форми з використанням рівностей 1 – 2:
Таким чином, отримана нормальна форма формули
. Аналогічно, з рівностей 3,4 отримаємо, що можна побудувати нормальну форму і для
. Нарешті, якщо відома нормальна форма
формули
, то нормальна форма
має вигляд:
Таким чином встановлено, що будь-яка формула логіки предикатів має нормальну форму.
Алгоритм приведення формули до нормальної форми
[ред. | ред. код]
Для приведення формули до нормальної форми потрібно виконати наступні операції:
- виключити операції
, ~, якщо вони є;
- зменшити область знаків заперечення;
- перейменувати змінні так, щоб можна було винести квантори в початок формули.