Bereinigte Normalform
# Bereinigte Normalform

In der Prädikatenlogik heißt eine Formel bereinigt, wenn

* keine Variable in der Formel einmal als freie und als gebundene Variable vorkommt,
* hinter jedem Quantor eine andere Variable steht.

Zu jeder Formel gibt es eine äquivalente bereinigte Formel. Jede Formel $F$ lässt sich durch geeignete, gebundene Umbenennung in eine bereinigte Form überführen.

## Beispiel

    $F:=\forall x\exists y\left(P\left(x,y\right)\wedge Q\left(x,z\right)\right)$
    $G:=\exists u\left(\forall vP\left(u,v\right)\vee Q\left(v,v\right)\right)$

In der Formel $F$ sind die Variablen $x$ und $y$ gebunden und $z$ ist frei. $F$ ist somit bereinigt. In der Formel $G$ sind alle Vorkommen der Variable $u$ gebunden, allerdings tritt $v$ sowohl gebunden als auch frei auf. $G$ ist daher nicht in bereinigter Form. Eine Überführung für $G$ ist folgende Umbenennung (bei der Umbenennung müssen die gebundenen Variablen umbenannt werden):

    $G':=\exists u\left(\forall wP\left(u,w\right)\vee Q\left(v,v\right)\right)$
