Нормальна форма формули у логіці предикатів — це формула, яка містить лише операції кон'юнкції, диз'юнкції та кванторні операції, а операція заперечення відноситься до елементарних формул.
З допомогою рівностей алгебри висловлень й логіки предикатів кожну формулу логіки предикатів можна привести до нормальної формули.[1]
Теорема:
Кожна формула логіки предикатів має нормальну форму.
Доведення:
Перш ніж доводити теорему, встановимо 4 равносильності, які необхідні нам надалі. В них передбачається, що формула Н не містить вільної змінної х:
Встановимо першу з цих рівносильностей. Решта - аналогічно.
Нехай істинна для деякої області М. Тоді на М істинно чи , чи . В першому випадку тотожно істинний на М предикат і через те, що не містить х, теж тотожно істинний на М предикат, і тоді - істинно. У другому випадку, якщо істинно , то істинно і незалежно від х, а значить з М.
Нехай тепер хибно. Тоді і хибні. Тобто існує , такий що хибно. Але тоді хибно, бо хибно.
Доведемо тепер теорему методом індукції. Для елементарних формул наше твердження істинне, бо вони самі є нормальними формами. Будь-яку формулу можна записати, використовуючи операції , тому достатньо показати, що якщо і мають нормальні форми, то і , , теж мають нормальні форми. Нехай і мають нормальні форми і , де
Тоді формулі рівносильна формула , яка може завжди бути приведена до нормальної форми з використанням рівностей 1 – 2:
Таким чином, отримана нормальна форма формули . Аналогічно, з рівностей 3,4 отримаємо, що можна побудувати нормальну форму і для . Нарешті, якщо відома нормальна форма формули , то нормальна форма має вигляд:
Таким чином встановлено, що будь-яка формула логіки предикатів має нормальну форму.
Алгоритм приведення формули до нормальної форми
[ред. | ред. код]
Для приведення формули до нормальної форми потрібно виконати наступні операції:
- виключити операції , ~, якщо вони є;
- зменшити область знаків заперечення;
- перейменувати змінні так, щоб можна було винести квантори в початок формули.