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

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

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

1. ${\displaystyle \forall xW(x)\lor H=\forall x(W(x)\lor H)}$
2. ${\displaystyle \exists xW(x)\lor H=\exists x(W(x)\lor H)}$
3. ${\displaystyle \forall xW(x)\land H=\forall x(W(x)\land H)}$
4. ${\displaystyle \exists xW(x)\land H=\exists x(W(x)\land H)}$

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

Нехай ${\displaystyle \forall xW(x)\lor H}$ істинна для деякої області М. Тоді на М істинно чи ${\displaystyle \forall xW(x)}$, чи ${\displaystyle H}$. В першому випадку ${\displaystyle W(x)}$ тотожно істинний на М предикат і через те, що ${\displaystyle H}$ не містить х, ${\displaystyle W(x)\lor H}$ теж тотожно істинний на М предикат, і тоді ${\displaystyle \forall xW(x)\lor H}$ - істинно. У другому випадку, якщо істинно ${\displaystyle H}$, то істинно і ${\displaystyle W(x)\lor H}$ незалежно від х, а значить ${\displaystyle \forall x}$ з М.

Нехай тепер ${\displaystyle \forall xW(x)\lor H}$ хибно. Тоді ${\displaystyle \forall xW(x)}$ і ${\displaystyle H}$ хибні. Тобто існує ${\displaystyle {x_{0}}\in M}$, такий що ${\displaystyle W(x_{0})}$ хибно. Але тоді ${\displaystyle W(x)\lor H}$ хибно, бо ${\displaystyle \forall xW(x)\lor H}$ хибно.

Доведемо тепер теорему методом індукції. Для елементарних формул наше твердження істинне, бо вони самі є нормальними формами. Будь-яку формулу можна записати, використовуючи операції ${\displaystyle \land ,\lor ,\neg ,}$, тому достатньо показати, що якщо ${\displaystyle W_{1}}$ і ${\displaystyle W_{2}}$ мають нормальні форми, то і ${\displaystyle \neg W_{1}}$, ${\displaystyle W_{1}\land W_{2}}$, ${\displaystyle W_{1}\lor W_{2}}$ теж мають нормальні форми. Нехай ${\displaystyle W_{1}}$ і ${\displaystyle W_{2}}$ мають нормальні форми ${\displaystyle {\widetilde {W_{1}}}}$ і ${\displaystyle {\widetilde {W_{2}}}}$, де

${\displaystyle {\widetilde {W_{1}}}=\forall x_{1}...\forall x_{i}\exists x_{i+1}...\exists x_{n}V_{1}(x_{1}...x_{n})}$

${\displaystyle {\widetilde {W_{1}}}=\exists y_{1}...\exists y_{i}\forall y_{i+1}...y_{m}V_{2}(y_{1}...y_{m})}$

Тоді формулі ${\displaystyle W_{1}\lor W_{2}}$ рівносильна формула ${\displaystyle {\widetilde {W_{1}}}\lor {\widetilde {W_{2}}}}$, яка може завжди бути приведена до нормальної форми з використанням рівностей 1 – 2:

${\displaystyle {\widetilde {W_{1}}}\lor {\widetilde {W_{2}}}=\forall x_{1}[\forall x_{2}...\forall x_{i}\exists x_{i+1}...\exists x_{n}V_{1}(x_{1}...x_{n})\lor \exists y_{1}...\exists y_{i}\forall y_{i+1}...y_{m}V_{2}(y_{1}...y_{m})]=\forall x_{1}...\forall x_{i}\exists x_{i+1}...\exists x_{n}\exists y_{1}...\exists y_{i}\forall y_{i+1}...y_{m}[V_{1}(x_{1}...x_{n})\lor V_{2}(y_{1}...y_{m})]}$

Таким чином, отримана нормальна форма формули ${\displaystyle W_{1}\lor W_{2}}$. Аналогічно, з рівностей 3,4 отримаємо, що можна побудувати нормальну форму і для ${\displaystyle W_{1}\land W_{2}}$. Нарешті, якщо відома нормальна форма ${\displaystyle {\widetilde {W_{1}}}}$ формули ${\displaystyle {W_{1}}}$, то нормальна форма ${\displaystyle {\overline {W_{1}}}}$ має вигляд:

${\displaystyle {\overline {W_{1}}}={\overline {\forall x_{1}...\forall x_{i}\exists x_{i+1}...\exists x_{n}V_{1}(x_{1}...x_{n})}}=\exists x_{1}...\exists x_{i}\forall x_{i+1}...\forall x_{n}{\overline {V_{1}(x_{1}...x_{n})}}}$

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

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

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

${\displaystyle \neg (\forall xP(x)\rightarrow \exists xQ(x))=\neg (\neg (\forall xP(x))\lor \exists xQ(x))=\forall xP(x)\land \forall x\neg Q(x)=\forall xP(x)\land \forall y\neg Q(y)=\forall x\forall yP(x)\neg Q(y)}$

• Алгоритмы приведения к нормальным формам (рус.)
• Префиксная нормальная форма (рус.)
• Основи логіки предикатів