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 <math>F</math> lässt sich durch geeignete, gebundene Umbenennung in eine bereinigte Form überführen.
Beispiel
- <math>F:=\forall x\exists y\left(P\left(x,y\right) \wedge Q\left(x,z\right)\right)</math>
- <math>G:=\exists u\left(\forall v P\left(u,v\right)\vee Q\left(v,v\right)\right)</math>
In der Formel <math>F</math> sind die Variablen <math>x</math> und <math>y</math> gebunden und <math>z</math> ist frei. <math>F</math> ist somit bereinigt. In der Formel <math>G</math> sind alle Vorkommen der Variable <math>u</math> gebunden, allerdings tritt <math>v</math> sowohl gebunden als auch frei auf. <math>G</math> ist daher nicht in bereinigter Form. Eine Überführung für <math>G</math> ist folgende Umbenennung (bei der Umbenennung müssen die gebundenen Variablen umbenannt werden):
- <math>G':=\exists u\left(\forall w P\left(u,w\right)\vee Q\left(v,v\right)\right)</math>