Satz prädikatenlogische Formel äquivalent zu PNF

Einfache Sprache

Satz prädikatenlogische Formel äquivalent zu PNF

Für jede Prädikatenlogische Formel existiert eine äquivalent Fromel in PNF.

Beweis: Wir nutzen Induktion, da Formeln in $\mathbf{PNF}$ induktiv definiert sind, über die Summe der Größen der Teilformeln, die nicht in PNF sind, geschrieben $w(\varphi)$.

IA: Sei $\varphi$ eine Formel mit $w(\varphi) = 0$. Dann ist $\varphi\in\mathbf{PNF}$, es keine Teilformel gibt die nicht in $\mathbf{PNF}$ ist.

IS: Sei $\varphi$ eine Formel mit $w(\varphi)> 0$. Sei $\psi$ eine Teilformel minimaler Größe, die nicht in $\mathbf{PNF}$ ist. Dann ist jede Teilformel von $\psi$ in $\mathbf{PNF}$, da sonst $\psi$ nicht minimale Größe hätte. Bemerke, dass $\psi$ nicht von der Form $Qx_i\psi'$ mit Quantor $Q$, da sonst $\psi$ in $\mathbf{PNF}$. Analog kann $\psi$ auch keine Atomare Formeln sein. Das ergibt Folgende Fälle:

Fall 1: Sei $\psi = \neg\psi_0$. Dann ist $\psi_0$ in $\mathbf{PNF}$. Würde $\psi_0$ quantorenfrei sein, dann wäre $\neg\psi_0$ bereits in $\mathbf{PNF}$, was einen Widerspruch dazu ist, dass $\psi$ eine Teilformel minimaler Größe ist, die nicht in $\mathbf{PNF}$ ist. Also muss $\psi_0 = Qx_i\psi_1$ für $Q\in\{\forall,\exists\}$. Dann ist $\psi$ äquivalent zu $\overline Qx_i\neg\psi_1$, wobei $\overline Q$ jeweils der andere Quantor ist. Da $w(\psi_1) IH anwenden und folgen, dass eine Formel $\chi$ existiert die zu äquivalent zu $\neg\psi_1$ und in $\mathbf{PNF}$ ist. Da Äquivalenz eine Kongruenzrelation ist, kann $\psi$ durch $\overline Qx_i\chi$ ersetzt werden. Wir erhalten. Die neue Formel $\varphi'$ mit mit $\psi$ ersetzt durch $\overline Qx_i\chi$ hat weniger Teilformen die nicht in $\mathbf{PNF}$ sind als noch $\varphi$. Wir können also wieder die IH anwenden und finden eine zu $\varphi'$ äquivalente Formel in $\mathbf{PNF}$.

Fall 2: Sei $\psi = \psi_0\lor\psi_1$. Dann ist $\psi_0$ und $\psi_1$ in $\mathbf{PNF}$ und mindestens eine von beiden beginnt mit einem Quantor. Nehmen wir o.B.d.A. an, dass $\psi_0 = Qx_i\psi_2$. Sei $j\in\mathbb N$ so, dass $x_j\not\in\mathrm{vars}(\varphi)$. Dann folgt die Äquivalenz

woraus wiederum

Nach der IH existiert eine Formel $\chi$ so, dass $\chi$ äquivalent zu $\psi_2\{x_i\mapsto x_j\}\lor\psi_1$ und in $\mathbf{PNF}$ ist. Jetzt können wir $\varphi$ durch $Qx_i\chi$ ersetzten und erhalten die äquivalente Formel $\varphi'$. Da $\varphi'$ weniger Teilformeln, die nicht in $\mathbf{PNF}$ sind, enthält, also $w(\varphi')IH eine zu $\varphi'$ äquivalente Formel existieren, die in $\mathbf{PNF}$ ist.

Fall 3: Sei $\psi = \psi_0\lor\psi_1$. Analog zu Fall 2. nur wird $\lor$ durch $\land$ ersetzt.

Algorithmus

  	\begin{algorithm}
	\caption{S-Formel-in-PNF-Algorithmus}
	\begin{algorithmic}
	\Input $\varphi\in\mathbf F_\textrm{PL}$
	\Output $\varphi'\in\mathbf{PNF}$
	\State $\varphi'\gets$ Rename variables in $\varphi$ such that no Quantifier has the same variable.
	\While{$\varphi'\not\in\mathbf{PNF}$}
	\State Find the smallest Subformula $\psi$ in $\varphi'$ with $\psi\not\in\mathbf{PNF}$. 
	\If{$\psi = \neg Qx_i\psi_0$}
	\State $\varphi'\gets$ $\varphi$ with $\psi$ replaced by $\overline Qx_i\neg\psi_0$.
	\Elif{$\psi = Qx_i\psi_0\land \psi_1$ \or $\psi =\psi_1\land  Qx_i\psi_0$}
	\State $\varphi'\gets \varphi'$ with $\psi$ replaced by $Qx_i(\psi_1\land \psi_0)$.
	\Elif{$\psi = Qx_i\psi_0\lor \psi_1$ \or $\psi =\psi_1\lor  Qx_i\psi_0$}
	\State $\varphi'\gets \varphi'$ with $\psi$ replaced by $Qx_i(\psi_1\lor \psi_0)$.
    \EndIf
    \EndWhile
    \Return $\varphi'$
	\end{algorithmic}
	\end{algorithm}

Formel in PNF bringen

Zuerst Variablen umbenennen so, dass für jede Quantifizierung eine andere Variable genutzt wird.

Example

Gegeben die Prädikatenlogische Formel $\varphi = P(x_2)\land\neg\forall x_0\forall x_1 E(x_0,x_1)$. Dann gilt

$$\begin{align}\varphi &\models=| P(x_2)\land\neg\forall x_0\forall x_1 E(x_0,x_1)\\&\models=| P(x_2)\land\exists x_0\neg\forall x_1 E(x_0,x_1)\\&\models=| P(x_2)\land\exists x_0\exists x_1\neg E(x_0,x_1)\\&\models=| \exists x_0(P(x_2)\land\exists x_1\neg E(x_0,x_1))\\&\models=| \exists x_0\exists x_1(P(x_2)\land\neg E(x_0,x_1))\\ \end{align}$$