Пренексна нормална форма (ПНФ)

Дефиниция (пренексна нормална форма)

Казваме, че формулата $\varphi$ е в ПНФ, ако:

(1)
\begin{align} \varphi = Q_1 x_1 \dots Q_n x_n \theta \end{align}

където:

  • $\theta$ е безкванторна формула;
  • $Q_1, \dots, Q_n$ са квантори;
  • $x_1, \dots, x_n$ са различни индивидни променливи.

Дефиниции (универсални и екзистенциални формули)

Нека $\varphi$ е в ПНФ и има вида $\forall x_1 \dots \forall x_n \theta$, където $\theta$ е безкванторна. Ще я наричаме универсална формула от тип $\Pi^0_1$.
Нека $\varphi$ е в ПНФ и има вида $\exists x_1 \dots \exists x_n \theta$, където $\theta$ е безкванторна. Ще я наричаме екзистенциална формула от тип $\Sigma^0_1$.
Нека $\varphi$ е в ПНФ и има вида $\forall x_1 \dots \forall x_n \theta$, където $\theta$ е от тип $\Sigma^0_{k-1}$. Ще я наричаме универсална формула от тип $\Pi^0_k$.
Нека $\varphi$ е в ПНФ и има вида $\exists x_1 \dots \exists x_n \theta$, където $\theta$ е от тип $\Pi^0_{k-1}$. Ще я наричаме екзистенциална формула от тип $\Sigma^0_k$.

Теорема (съществуване на алгоритъм за преобразуване в ПНФ)

Има алгоритъм $\mathbb{A}$, който за всяка предикатна формула $\varphi$ завършва за краен брой стъпки и дава резултат $\mathbb{A}(\varphi)$, като:
(i) $\mathrm{Var}^{free}[\varphi] = \mathrm{Var}^{free}[\mathbb{A}(\varphi)]$;
(ii) $\varphi |=| \mathbb{A}(\varphi)$;
(iii) $\mathbb{A}(\varphi)$ е в ПНФ.

Лема 1

Ако може да намерим ефективно ПНФ на $\varphi$, то може да намерим ПНФ на $\lnot \varphi$.
Ако $\mathbb{A}(\varphi) = Q_1 x_1 \dots Q_n x_n \theta$ - ПНФ.
Дефинираме $\mathbb{A}(\lnot \varphi) \rightleftharpoons Q_1^\sigma x_1 \dots Q_n^\sigma x_n \lnot \theta$, където $\forall^\sigma = \exists$, $\exists^\sigma = \forall$.
Ще докажем, че са изпълнени 3те условия:
$\varphi |=| \mathbb{A}(\varphi)$ - от допускането за $\varphi$. Слaгаме отрицание от 2те страни:

(2)
\begin{eqnarray} \lnot \varphi &|=|& \lnot \mathbb{A}(\varphi) \\ &|=|& \lnot Q_1 x_1 \dots Q_n x_n \theta \\ &|=|& Q_1^\sigma x_1 \lnot Q_2 x_2 \dots Q_n x_n \theta \\ &\vdots& \\ &|=|& Q_1^\sigma x_1 Q_2^\sigma x_2 \dots Q_n^\sigma x_n \lnot \theta \\ &|=|& \mathbb{A}(\lnot \varphi) \\ \end{eqnarray}

с това лемата е доказана.

Лема 2

Ако може ефективно да намерим ПНФ на $\varphi, \psi$ то ефективно може да намерим ПНФ на $\varphi \sigma \psi$, където $\sigma \in \{ \And, \lor \}$.
Доказателство: Нека

(3)
\begin{eqnarray} \mathbb{A}(\varphi) &=& Q_1 x_1 \dots Q_n x_n \theta \\ \mathbb{A}(\psi) &=& K_1 y_1 \dots K_l y_l \chi \\ \end{eqnarray}

Избираме си различни индивидни променливи $x_1', \dots, x_n', y_1', \dots, y_l'$, които са различни от всички променливи, които се срещат в $\mathbb{A}(\varphi) \sigma \mathbb{A}(\psi)$.
Ще преименуваме свързаните променливи и ще изнесем кванторите напред:

(4)
\begin{eqnarray} Q_1 x_1 \dots Q_n x_n \theta\ \sigma\ K_1 y_1 \dots K_l y_l \chi &|=|& Q_1 x_1' \dots Q_n x_n' \theta[x_1/x_1', \dots, x_n/x_n']\ \sigma\ K_1 y_1' \dots K_l y_l' \chi[y_1/y_1', \dots, y_l/y_l'] \\ &|=|& Q_1 x_1' (Q_2 x_2' \dots Q_n x_n' \theta[x_1/x_1', \dots, x_n/x_n']\ \sigma\ K_1 y_1' \dots K_l y_l' \chi[y_1/y_1', \dots, y_l/y_l']) \\ &|=|& Q_1 x_1' \dots Q_n x_n' (\theta[x_1/x_1', \dots, x_n/x_n']\ \sigma\ K_1 y_1' \dots K_l y_l' \chi[y_1/y_1', \dots, y_l/y_l']) \\ &|=|& Q_1 x_1' \dots Q_n x_n' K_1 y_1' (\theta[x_1/x_1', \dots, x_n/x_n']\ \sigma\ K_2 y_2' \dots K_l y_l' \chi[y_1/y_1', \dots, y_l/y_l']) \\ &|=|& Q_1 x_1' \dots Q_n x_n' K_1 y_1' \dots K_l y_l' (\theta[x_1/x_1', \dots, x_n/x_n']\ \sigma\ \chi[y_1/y_1', \dots, y_l/y_l']) \\ &\rightleftharpoons& \mathbb{A}(\varphi\ \sigma\ \psi) \\ \end{eqnarray}

Доказателство(на теоремата):
Ще направим индукция по построението на формулата $\varphi$:
(1) $\varphi = \lnot \psi$, където за $\psi$ твърдението е доказано. Използваме Лема 1.
(2) $\varphi = \psi_1 \sigma \psi_2$, където за $\psi_1, \psi_2$ твърдението е доказано. Използваме Лема 2.
(3) $\varphi = \psi_1 \Rightarrow \psi_2$, където за $\psi_1, \psi_2$ твърдението е доказано.
Използваме:

(5)
\begin{align} \varphi |=| \underbrace{\underbrace{\lnot \psi_1}_{L1} \lor \psi_2}_{L2} \end{align}

(4) $\varphi = \psi_1 \iff \psi_2$, където за $\psi_1, \psi_2$ твърденето е доказано. Използваме:

(6)
\begin{align} \psi_1 \iff \psi_2 |=| \underbrace{\underbrace{(\psi_1 \And \psi_2)}_{L2} \lor \underbrace{(\underbrace{\lnot \psi_1}_{L1} \And \underbrace{\lnot \psi_2}_{L1})}_{L2}}_{L2} \end{align}

(5) $\varphi = Qx\psi$, където за $\psi$ твърдението е доказано.
Нека $\mathbb{A}(\psi) = Q_1 x_1 \dots Q_n x_n \theta$, където $\theta$ е безкванторна. Разглеждаме 2 случая:
(5.1) $x \in \{ x_1, \dots, x_n \}$, тогава $\mathbb{A}(Qx\psi) = \mathbb{A}(\psi)$
(5.2) $x \notin \{ x_1, \dots, x_n \}$, тогава $\mathbb{A}(Qx\psi) = Qx\mathbb{A}(\psi)$

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-NonCommercial-ShareAlike 3.0 License